totallyDisconnectedSpace_iff_connectedComponent_singleton

English

For a totally disconnected space, the connected component of any point is the singleton {x}.

Русский

Для полностью раздельного пространства компонент связности любой точки равен единственному элементу: {x}.

LaTeX

$$$\forall x: \alpha, connectedComponent x = { x }$$$

Lean4

/-- A space is totally disconnected iff its connected components are singletons. -/
theorem totallyDisconnectedSpace_iff_connectedComponent_singleton :
    TotallyDisconnectedSpace α ↔ ∀ x : α, connectedComponent x = { x } :=
  by
  rw [totallyDisconnectedSpace_iff_connectedComponent_subsingleton]
  refine forall_congr' fun x => ?_
  rw [subsingleton_iff_singleton]
  exact mem_connectedComponent

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