Helper Lemmas about the Kleene Star #
Useful results about the reflexive-transitive closure ReflTransGen and TransGen.
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
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 : α}
:
ReflTransGen r a b → 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 : α}
:
ReflTransGen r a b → 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) → ReflTransGen r a b → ReflTransGen r' a b