Union_of_Connected_Sets_with_Non_Empty_Intersections_is_Connected
Provedconnected-spacesproofwikiunion-of-connected-sets-with-non-empty-intersections-is-connected
Let be a topological space. Let be an indexing set. Let be an indexed family of subsets of , all connected in . Let be such that no two of its elements are disjoint Then is itself connected.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Union_of_Connected_Sets_with_Non_Empty_Intersections_is_Connected {α : Type _} [TopologicalSpace α] {s t : Set α} (hs : IsConnected s) (ht : IsConnected t) (hst : (s ∩ t).Nonempty) : IsConnected (s ∪ t) := by sorrySource