English
The disjoint union (sum) of two totally disconnected spaces is totally disconnected.
Русский
Дисъюнктное объединение двух полностью раздельных пространств вновь является полностью раздельным пространством.
LaTeX
$$$TotallyDisconnectedSpace(\alpha) \land TotallyDisconnectedSpace(\beta) \Rightarrow TotallyDisconnectedSpace( Sum \\alpha \\beta)$$$
Lean4
instance [TopologicalSpace β] [TotallyDisconnectedSpace α] [TotallyDisconnectedSpace β] :
TotallyDisconnectedSpace (α ⊕ β) := by
refine ⟨fun s _ hs => ?_⟩
obtain ⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩ := Sum.isPreconnected_iff.1 hs
· exact ht.subsingleton.image _
· exact ht.subsingleton.image _