English
The flattening of a list of lists is an IsChain iff every inner list is an IsChain and consecutive inner lists are linked by the chain condition via their ends and heads.
Русский
Посплитение списка списков образует цепь, если каждая внутренняя цепь образует цепь и соседние списки соединяются нормально через последний элемент одного и первый элемент другого.
LaTeX
$$$IsChain\\, R\\, L.flatten \\iff (\\forall l \\in L, IsChain\\, R\\, l) \\land IsChain\\, (\\\\lambda l_1 l_2, \\forall x \\in l_1.max, \\forall y \\in l_2.head, R\\ x\\ y)\\, L$$$
Lean4
theorem isChain_flatten :
∀ {L : List (List α)},
[] ∉ L →
(IsChain R L.flatten ↔
(∀ l ∈ L, IsChain R l) ∧ L.IsChain (fun l₁ l₂ => ∀ᵉ (x ∈ l₁.getLast?) (y ∈ l₂.head?), R x y))
| [], _ => by simp
| [l], _ => by simp [flatten]
| (l₁ :: l₂ :: L), hL => by
rw [mem_cons, not_or, ← Ne] at hL
rw [flatten, isChain_append, isChain_flatten hL.2, forall_mem_cons, isChain_cons_cons]
rw [mem_cons, not_or, ← Ne] at hL
simp only [forall_mem_cons, and_assoc, flatten, head?_append_of_ne_nil _ hL.2.1.symm]
exact Iff.rfl.and (Iff.rfl.and <| Iff.rfl.and and_comm)
