English
The directed sUnion of a family of preconnected subsets is preconnected.
Русский
Направленное sUnion семейства предсоединённых подмножеств предсоединено.
LaTeX
$$$$ \\forall S,\\ \\operatorname{DirectedOn}(\\,\\cdot \\subseteq \\cdot\\,)\n S \\Rightarrow (\\forall s \\in S, \\operatorname{IsPreconnected}(s)) \\Rightarrow \\operatorname{IsPreconnected}(\\bigcup S). $$$$
Lean4
theorem union {s t : Set α} (H : (s ∩ t).Nonempty) (Hs : IsConnected s) (Ht : IsConnected t) : IsConnected (s ∪ t) :=
by
rcases H with ⟨x, hx⟩
refine ⟨⟨x, mem_union_left t (mem_of_mem_inter_left hx)⟩, ?_⟩
exact Hs.isPreconnected.union x (mem_of_mem_inter_left hx) (mem_of_mem_inter_right hx) Ht.isPreconnected
