English
The iUnion of connected sets indexed by a chain (type with archimedean successor) is connected provided neighboring sets meet.
Русский
iUnion связанных множеств, индексируемых цепью, связно при условии, что соседние множества пересекаются.
LaTeX
$$$$ \\forall \\text{β},\\; [Nonempty \\ β] \\Rightarrow \\{s_n\\}_{n\\in β} \\text{ связны} \\wedge (s_n \\cap s_{\\operatorname{succ} n}).Nonempty \\Rightarrow \\operatorname{IsConnected}(\\bigcup_n s_n). $$$$
Lean4
/-- The iUnion of connected sets indexed by a type with an archimedean successor (like `ℕ` or `ℤ`)
such that any two neighboring sets meet is preconnected. -/
theorem iUnion_of_chain {s : β → Set α} (H : ∀ n, IsPreconnected (s n)) (K : ∀ n, (s n ∩ s (succ n)).Nonempty) :
IsPreconnected (⋃ n, s n) :=
IsPreconnected.iUnion_of_reflTransGen H fun _ _ =>
reflTransGen_of_succ _ (fun i _ => K i) fun i _ =>
by
rw [inter_comm]
exact K i
