English
If a family of sets {s_i} is such that each s_i is preconnected and they all contain a common point x, then the union ⋃ s_i is preconnected.
Русский
Если семейство множеств {s_i} содержит общее место x и каждое s_i предсоединено, то объединение ⋃ s_i предсоединено.
LaTeX
$$$$ \\forall x,\\forall i\\in C,\\operatorname{IsPreconnected}(s_i) \\Rightarrow \\operatorname{IsPreconnected}\\left(\\bigcup_{i\\in C} s_i\\right). $$$$
Lean4
/-- A union of a family of preconnected sets with a common point is preconnected as well. -/
theorem isPreconnected_sUnion (x : α) (c : Set (Set α)) (H1 : ∀ s ∈ c, x ∈ s) (H2 : ∀ s ∈ c, IsPreconnected s) :
IsPreconnected (⋃₀ c) := by
apply isPreconnected_of_forall x
rintro y ⟨s, sc, ys⟩
exact ⟨s, subset_sUnion_of_mem sc, H1 s sc, ys, H2 s sc⟩
