instTotallyDisconnectedSpaceSum — Mathlib

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 _

Похожие утверждения