English
If there is a chain from a to b under the reflexive transitive closure of a relation, there exists a finite list starting at a and ending at b forming an IsChain.
Русский
Если существует цепь между a и b относительно рефлексивного транзитивного замыкания отношения, существует конечный список от a к b, образующий IsChain.
LaTeX
$$$\\exists l,\\ IsChain\\, r\\, (a :: l) \\land getLast (a :: l) (cons_ne_nil _) = b $$$
Lean4
/-- If `a` and `b` are related by the reflexive transitive closure of `r`, then there is an
`r`-chain starting from `a` and ending on `b`.
-/
theorem exists_isChain_cons_of_relationReflTransGen (h : Relation.ReflTransGen r a b) :
∃ l, IsChain r (a :: l) ∧ getLast (a :: l) (cons_ne_nil _ _) = b :=
by
refine Relation.ReflTransGen.head_induction_on h ?_ ?_
· exact ⟨[], .singleton _, rfl⟩
· intro c d e _ ih
obtain ⟨l, hl₁, hl₂⟩ := ih
refine ⟨d :: l, .cons_cons e hl₁, ?_⟩
rwa [getLast_cons_cons]
