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