English
The iUnion of preconnected sets indexed by a type with a successor, such that any two neighboring sets meet, is preconnected.
Русский
Объединение iUnion предсоединённых множеств, индексируемых по типу с продолжателем, где любые соседние множества пересекаются, предсоединено.
LaTeX
$$$$ \\forall n, (s_n) \\text{ предсоединено},\\ (s_n \\cap s_{\\operatorname{succ} n}).Nonempty \\Rightarrow \\operatorname{IsPreconnected}(\\bigcup_n s_n). $$$$
Lean4
/-- Preconnectedness of the iUnion of a family of preconnected sets
indexed by the vertices of a preconnected graph,
where two vertices are joined when the corresponding sets intersect. -/
theorem iUnion_of_reflTransGen {ι : Type*} {s : ι → Set α} (H : ∀ i, IsPreconnected (s i))
(K : ∀ i j, ReflTransGen (fun i j : ι => (s i ∩ s j).Nonempty) i j) : IsPreconnected (⋃ n, s n) :=
by
rw [← biUnion_univ]
exact IsPreconnected.biUnion_of_reflTransGen (fun i _ => H i) fun i _ j _ => by simpa [mem_univ] using K i j
