totallyDisconnectedSpace — Mathlib

English

The space of connected components of any space α, denoted ConnectedComponents(α), is totally disconnected.

Русский

Пространство компонент связности пространства α, то есть ConnectedComponents(α), полностью раздельно.

LaTeX

$$$\text{TotallyDisconnectedSpace}(\mathrm{ConnectedComponents}(\alpha))$$$

Lean4

instance totallyDisconnectedSpace : TotallyDisconnectedSpace (ConnectedComponents α) :=
  by
  rw [totallyDisconnectedSpace_iff_connectedComponent_singleton]
  refine ConnectedComponents.surjective_coe.forall.2 fun x => ?_
  rw [← ConnectedComponents.isQuotientMap_coe.image_connectedComponent, ← connectedComponents_preimage_singleton,
    image_preimage_eq _ ConnectedComponents.surjective_coe]
  refine ConnectedComponents.surjective_coe.forall.2 fun y => ?_
  rw [connectedComponents_preimage_singleton]
  exact isConnected_connectedComponent

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