English
If s ∩ t is nonempty and s,t are connected, then s ∪ t is connected.
Русский
Если s ∩ t непусто и s,t связаны, то s ∪ t связанно.
LaTeX
$$$$ (s \\cap t) \\neq \\varnothing \\wedge \\operatorname{IsConnected}(s) \\wedge \\operatorname{IsConnected}(t) \\Rightarrow \\operatorname{IsConnected}(s \\cup t). $$$$
Lean4
/-- The directed sUnion of a set S of preconnected subsets is preconnected. -/
theorem sUnion_directed {S : Set (Set α)} (K : DirectedOn (· ⊆ ·) S) (H : ∀ s ∈ S, IsPreconnected s) :
IsPreconnected (⋃₀ S) :=
by
rintro u v hu hv Huv ⟨a, ⟨s, hsS, has⟩, hau⟩ ⟨b, ⟨t, htS, hbt⟩, hbv⟩
obtain ⟨r, hrS, hsr, htr⟩ : ∃ r ∈ S, s ⊆ r ∧ t ⊆ r := K s hsS t htS
have Hnuv : (r ∩ (u ∩ v)).Nonempty :=
H _ hrS u v hu hv ((subset_sUnion_of_mem hrS).trans Huv) ⟨a, hsr has, hau⟩ ⟨b, htr hbt, hbv⟩
have Kruv : r ∩ (u ∩ v) ⊆ ⋃₀ S ∩ (u ∩ v) := inter_subset_inter_left _ (subset_sUnion_of_mem hrS)
exact Hnuv.mono Kruv
