nhdsNE_neBot — Mathlib

English

For any X with a basis property of non-emptiness near nonunique points, a similar nontrivial neighborhood persists in OnePoint X.

Русский

При наличии базиса неотрицательных окрестностей в X сохраняется нетривиальная окрестность и в OnePoint X.

LaTeX

$$$\text{For all } X, (\text{nhdsWithin } x (\operatorname{compl} \{x\}))^\text{NeBot} \Rightarrow (\text{nhdsWithin } x (\operatorname{compl} \{\operatorname{OnePoint}.some x\}))^\text{NeBot}$$$

Lean4

instance (priority := 900) nhdsNE_neBot [∀ x : X, NeBot (𝓝[≠] x)] [NoncompactSpace X] (x : OnePoint X) :
    NeBot (𝓝[≠] x) :=
  OnePoint.rec OnePoint.nhdsNE_infty_neBot (fun y => OnePoint.nhdsNE_coe_neBot y) x

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