def Rel.iterate {α : Type u_1} (R : Rel α α) : ℕ → α → α → Prop

Equations

• R.iterate 0 = fun (x x_1 : α) => x = x_1
• R.iterate n.succ = fun (x y : α) => ∃ (z : α), R x z ∧ R.iterate n z y

@[simp]

theorem Rel.iterate.iff_zero {α : Type u_1} {R : Rel α α} {x : α} {y : α} : R.iterate 0 x y ↔ x = y

@[simp]

theorem Rel.iterate.iff_succ {α : Type u_1} {R : Rel α α} {n : ℕ} {x : α} {y : α} : R.iterate (n + 1) x y ↔ ∃ (z : α), R x z ∧ R.iterate n z y

@[simp]

theorem Rel.iterate.eq {α : Type u_1} {n : ℕ} : Rel.iterate (fun (x x_1 : α) => x = x_1) n = fun (x x_1 : α) => x = x_1

theorem Rel.iterate.forward {α : Type u_1} {R : Rel α α} {n : ℕ} {x : α} {y : α} : R.iterate (n + 1) x y ↔ ∃ (z : α), R.iterate n x z ∧ R z y

theorem Rel.iterate.true_any {n : ℕ} : ∀ {α : Type u_1} {x y : α}, x = y → Rel.iterate (fun (x x : α) => True) n x y