connectedComponent_eq_singleton — Mathlib

English

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

Русский

В полностью раздельном пространстве связанный компонент любой точки равен {x}.

LaTeX

$$$∀ x: α, connectedComponent x = { x }$$$

Lean4

@[simp]
theorem connectedComponent_eq_singleton [TotallyDisconnectedSpace α] (x : α) : connectedComponent x = { x } :=
  totallyDisconnectedSpace_iff_connectedComponent_singleton.1 ‹_› x

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