English
The biUnion of a family of connected sets is connected if the index graph is connected.
Русский
би-объединение семейства связанных множеств связано, если граф индексов связан.
LaTeX
$$$$ \\forall \\text{{α}},\\forall {ι},\\forall t\\subseteq ι,\\forall s: ι\\to \\mathcal P(α),\\n\\text{ если } \\dots \\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 α} (H : ∀ i ∈ t, IsPreconnected (s i))
(K : ∀ i, i ∈ t → ∀ j, j ∈ t → ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j) :
IsPreconnected (⋃ n ∈ t, s n) :=
by
let R := fun i j : ι => (s i ∩ s j).Nonempty ∧ i ∈ t
have P : ∀ i, i ∈ t → ∀ j, j ∈ t → ReflTransGen R i j → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j) :=
fun i hi j hj h => by
induction h with
| refl =>
refine ⟨{ i }, singleton_subset_iff.mpr hi, mem_singleton i, mem_singleton i, ?_⟩
rw [biUnion_singleton]
exact H i hi
| @tail j k _ hjk ih =>
obtain ⟨p, hpt, hip, hjp, hp⟩ := ih hjk.2
refine ⟨insert k p, insert_subset_iff.mpr ⟨hj, hpt⟩, mem_insert_of_mem k hip, mem_insert k p, ?_⟩
rw [biUnion_insert]
refine (H k hj).union' (hjk.1.mono ?_) hp
rw [inter_comm]
exact inter_subset_inter_right _ (subset_biUnion_of_mem hjp)
refine isPreconnected_of_forall_pair ?_
intro x hx y hy
obtain ⟨i : ι, hi : i ∈ t, hxi : x ∈ s i⟩ := mem_iUnion₂.1 hx
obtain ⟨j : ι, hj : j ∈ t, hyj : y ∈ s j⟩ := mem_iUnion₂.1 hy
obtain ⟨p, hpt, hip, hjp, hp⟩ := P i hi j hj (K i hi j hj)
exact ⟨⋃ j ∈ p, s j, biUnion_subset_biUnion_left hpt, mem_biUnion hip hxi, mem_biUnion hjp hyj, hp⟩
