English
IsChain R (l1 ++ l2) is equivalent to IsChain R l1 and IsChain R l2 together with a cross-term condition relating the last element of l1 and the first element of l2.
Русский
IsChain R (l1 ++ l2) эквивалентно IsChain R l1 и IsChain R l2 вместе с кросс-условием между последним элементом l1 и первым элементом l2.
LaTeX
$$IsChain R (l1 ++ l2) ↔ IsChain R l1 ∧ IsChain R l2 ∧ ∀ x ∈ l1.getLast?, ∀ y ∈ l2.head?, R x y$$
Lean4
theorem isChain_append :
∀ {l₁ l₂ : List α}, IsChain R (l₁ ++ l₂) ↔ IsChain R l₁ ∧ IsChain R l₂ ∧ ∀ x ∈ l₁.getLast?, ∀ y ∈ l₂.head?, R x y
| [], l => by simp
| [a], l => by simp [isChain_cons', and_comm]
| a :: b :: l₁, l₂ =>
by
rw [cons_append, cons_append, isChain_cons_cons, isChain_cons_cons, ← cons_append, isChain_append, and_assoc]
simp
