English
If a list is an IsChain, then any two end points in the list are connected by the reflexive transitive closure of the relation.
Русский
Если список образует IsChain, то концы списка связаны через рефлексивное транзитивное замыкание отношения.
LaTeX
$$$\\forall l, IsChain\\, r\\, l \\rightarrow \\forall hne, \\text{head} l \\to \\text{getLast} l \\;\\text{через ReflTransGen } r$$$
Lean4
/-- If there is an non-empty `r`-chain, its head and last element are related by the
reflexive transitive closure of `r`.
-/
theorem relationReflTransGen_of_exists_isChain (l : List α) (hl₁ : IsChain r l) (hne : l ≠ []) :
Relation.ReflTransGen r (head l hne) (getLast l hne) :=
IsChain.induction (Relation.ReflTransGen r (head l hne) ·) l hl₁ (fun _ _ h₁ h₂ => Trans.trans h₂ h₁)
(fun _ => Relation.ReflTransGen.refl) _ (getLast_mem _)
