isClopen_connectedComponent — Mathlib

English

In a locally connected space, the connected component of a point is both closed and open (clopen).

Русский

В локально связном пространстве связная компонентa точки является одновременно открытым и закрытым (clopen).

LaTeX

$$isClopen_connectedComponent$$

Lean4

theorem isClopen_connectedComponent [LocallyConnectedSpace α] {x : α} : IsClopen (connectedComponent x) :=
  ⟨isClosed_connectedComponent, isOpen_connectedComponent⟩

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