exists_isChain_ne_nil_of_relationReflTransGen

English

Same as above, with explicit head and tail construction; there exists a nonempty chain from head to last.

Русский

То же самое, но явная конструкция головы и хвоста; существует непустая цепь от головы до последнего элемента.

LaTeX

$$$\\exists l, \\exists hl, IsChain\\, r\\, l \\land l.head hl = a \\land l.getLast hl = 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_ne_nil_of_relationReflTransGen (h : Relation.ReflTransGen r a b) :
    ∃ l, ∃ (hl : l ≠ []), IsChain r l ∧ l.head hl = a ∧ getLast l hl = b := by
  rcases exists_isChain_cons_of_relationReflTransGen h with ⟨l, _⟩; use (a :: l); grind

Похожие утверждения