English
If a and b are related by the reflexive transitive closure, then there exists an IsChain starting at a and ending at b with a supporting tail.
Русский
Если a и b связаны через рефлексивно транзитивное замыкание, существует цепь IsChain от a до b с хвостом.
LaTeX
$$$\\forall a,b, \\text{Relation.ReflTransGen } r \\ a \\ b \\Rightarrow \\exists l, IsChain r (a :: l) \\land getLast (a :: l) (cons_ne_nil _) = b$$$
Lean4
/-- If there is an `r`-chain starting from `a` and ending at `b`, then `a` and `b` are related by the
reflexive transitive closure of `r`.
-/
theorem relationReflTransGen_of_exists_isChain_cons (l : List α) (hl₁ : IsChain r (a :: l))
(hl₂ : getLast (a :: l) (cons_ne_nil _ _) = b) : Relation.ReflTransGen r a b :=
IsChain.backwards_cons_induction_head _ l hl₁ hl₂ (fun _ _ => Relation.ReflTransGen.head) Relation.ReflTransGen.refl
