isOpen_connectedComponent — Mathlib

English

In a locally connected space, the connected component of any point is an open set.

Русский

В локально связном пространстве связная компонентa любой точки является открытым множеством.

LaTeX

$$isOpen_connectedComponent$$

Lean4

theorem isOpen_connectedComponent [LocallyConnectedSpace α] {x : α} : IsOpen (connectedComponent x) :=
  by
  rw [← connectedComponentIn_univ]
  exact isOpen_univ.connectedComponentIn

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