theorem
ReflTransGen.cases_tail_eq_neq
{α : Type u_1}
{x z : α}
{r : α → α → Prop}
(h : Relation.ReflTransGen r x z)
:
A version of Relation.ReflTransGen.cases_tail also giving (in)equalities.
theorem
ReflTransGen.to_finitelyManySteps
{α : Type u_1}
{x z : α}
{r : α → α → Prop}
(h : Relation.ReflTransGen r x z)
:
∃ x₀ ... xₙ, a = x₀ ∧ r x₀ x₁ ∧ ... ∧ xₙ = b implies ReflTransGen r a b
theorem
ReflTransGen.from_finitelyManySteps
{α : Type u_1}
(r : α → α → Prop)
{n : ℕ}
(x z : α)
(ys : List.Vector α n.succ)
:
ReflTransGen r a b implies that ∃ x₀ ... xₙ, a = x₀ ∧ r x₀ x₁ ∧ ... ∧ xₙ = b
theorem
ReflTransGen.iff_finitelyManySteps
{α : Type u_1}
(r : α → α → Prop)
(x z : α)
:
Relation.ReflTransGen r x z ↔ ∃ (n : ℕ) (ys : List.Vector α n.succ),
x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)
ReflTransGen r a b is equivalent to ∃ x₀ ... xₙ, a = x₀ ∧ r x₀ x₁ ∧ ... ∧ r xₙ = b
theorem
Relation.ReflTransGen_or_left
{α : Type u_1}
{r r' : α → α → Prop}
{a b : α}
:
Relation.ReflTransGen r a b → Relation.ReflTransGen (fun (x y : α) => r x y ∨ r' x y) a b
theorem
Relation.ReflTransGen_or_right
{α : Type u_1}
{r r' : α → α → Prop}
{a b : α}
:
Relation.ReflTransGen r a b → Relation.ReflTransGen (fun (x y : α) => r' x y ∨ r x y) a b
theorem
Relation.ReflTransGen_imp
{α : Type u_1}
{r r' : α → α → Prop}
{a b : α}
:
(∀ (x y : α), r x y → r' x y) → Relation.ReflTransGen r a b → Relation.ReflTransGen r' a b
theorem
Relation.TransGen_or_left
{α : Sort u_1}
{r r' : α → α → Prop}
{a b : α}
:
Relation.TransGen r a b → Relation.TransGen (fun (x y : α) => r x y ∨ r' x y) a b
theorem
Relation.TransGen_or_right
{α : Sort u_1}
{r r' : α → α → Prop}
{a b : α}
:
Relation.TransGen r a b → Relation.TransGen (fun (x y : α) => r' x y ∨ r x y) a b
theorem
Relation.TransGen_imp
{α : Sort u_1}
{r r' : α → α → Prop}
{a b : α}
:
(∀ (x y : α), r x y → r' x y) → Relation.TransGen r a b → Relation.TransGen r' a b