English
Let s: β → Set α and t ⊆ β be nonempty and OrdConnected. If every s(n) is connected and for every n ∈ t with succ n ∈ t we have s(n) ∩ s(succ n) ≠ ∅, then the union over n ∈ t of s(n) is connected.
Русский
Пусть s: β → множества α и t ⊆ β непусто, и т‡ord-connected. Пусть каждый s(n) связан, и для каждого n ∈ t с succ n ∈ t выполняется s(n) ∩ s(succ(n)) ≠ ∅. Тогда объединение ⋃_{n∈t} s(n) связано.
LaTeX
$$$\\forall s : β \\to \\mathcal{P}(α), \\forall t \\subseteq β, t \\neq \\emptyset \\land OrdConnected(t) \\land (\\forall n \\in t, IsConnected(s(n))) \\land (\\forall n \\in t, succ(n) \\in t \\Rightarrow (s(n) \\cap s(succ(n))) \\neq \\varnothing) \\Rightarrow IsConnected \\left( \\bigcup_{n \\in t} s(n) \\right)$$$
Lean4
/-- The iUnion of connected sets indexed by a subset of a type with an archimedean successor
(like `ℕ` or `ℤ`) such that any two neighboring sets meet is preconnected. -/
theorem biUnion_of_chain {s : β → Set α} {t : Set β} (hnt : t.Nonempty) (ht : OrdConnected t)
(H : ∀ n ∈ t, IsConnected (s n)) (K : ∀ n : β, n ∈ t → succ n ∈ t → (s n ∩ s (succ n)).Nonempty) :
IsConnected (⋃ n ∈ t, s n) :=
⟨nonempty_biUnion.2 <| ⟨hnt.some, hnt.some_mem, (H _ hnt.some_mem).nonempty⟩,
IsPreconnected.biUnion_of_chain ht (fun i hi => (H i hi).isPreconnected) K⟩
