English
A chain on a list built by attaching elements with a predicate p corresponds to a chain on the underlying list with an existential link between consecutive elements.
Русский
Цепь на списке, построенном с помощью attachWith и предиката p, соответствует цепи на базовом списке со связью между соседними элементами, выраженной через существование; между элементами в связке существует некоторый элемент, удовлетворяющий p.
LaTeX
$$$IsChain\\, r\\, (l.attachWith\\ p\\ h) \\iff IsChain\\, (\\lambda a,b,\\exists ha,\\exists hb, r\\, ⟨a,ha⟩, ⟨b,hb⟩)\\, l$$$
Lean4
/-- If `l₁ l₂` and `l₃` are lists and `l₁ ++ l₂` and `l₂ ++ l₃` both satisfy
`IsChain R`, then so does `l₁ ++ l₂ ++ l₃` provided `l₂ ≠ []` -/
theorem append_overlap {l₁ l₂ l₃ : List α} (h₁ : IsChain R (l₁ ++ l₂)) (h₂ : IsChain R (l₂ ++ l₃)) (hn : l₂ ≠ []) :
IsChain R (l₁ ++ l₂ ++ l₃) :=
h₁.append h₂.right_of_append <| by simpa only [getLast?_append_of_ne_nil _ hn] using (isChain_append.1 h₂).2.2
