English
The biUnion of a family of connected sets is connected if the index graph formed by pairwise intersections is connected.
Русский
биобъединение семейства связанных множеств связано, если граф индексов, образованный пересечениями, связан.
LaTeX
$$$$ \\forall \\text{α},\\forall s: ι \\to Set α,\\ \\text{Ht},\\ldots \\Rightarrow \\operatorname{IsConnected}(\\bigcup_{n\\in t} s_n). $$$$
Lean4
/-- The biUnion of a family of preconnected sets is preconnected if the graph determined by
whether two sets intersect is preconnected. -/
theorem biUnion_of_reflTransGen {ι : Type*} {t : Set ι} {s : ι → Set α} (ht : t.Nonempty)
(H : ∀ i ∈ t, IsConnected (s i))
(K : ∀ i, i ∈ t → ∀ j, j ∈ t → ReflTransGen (fun i j : ι => (s i ∩ s j).Nonempty ∧ i ∈ t) i j) :
IsConnected (⋃ n ∈ t, s n) :=
⟨nonempty_biUnion.2 <| ⟨ht.some, ht.some_mem, (H _ ht.some_mem).nonempty⟩,
IsPreconnected.biUnion_of_reflTransGen (fun i hi => (H i hi).isPreconnected) K⟩
