not_isolated — Mathlib

English

In a perfect space, every point has a nontrivial punctured neighborhood; equivalently, each nhds within the punctured space is nonempty.

Русский

В совершенном пространстве каждая точка имеет непустую окрестность без самой точки.

LaTeX

$$$[\text{PerfectSpace } X] \Rightarrow \forall x, \big( \mathcal{N}_{x}^{\neq} \big).\text{NeBot}.$$$

Lean4

instance not_isolated [PerfectSpace X] (x : X) : Filter.NeBot (𝓝[≠] x) :=
  perfectSpace_iff_forall_not_isolated.mp ‹_› x

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