nhdsNE_coe_neBot — Mathlib

English

If x ∈ X has a nontrivial neighborhood filter 𝓝[≠] x, then the corresponding point x in OnePoint X also has a nontrivial 𝓝[≠].

Русский

Если у x в X не тривиальная локальная окрестность, то соответствующая точка в OnePoint X тоже не имеет тривиальных окрестностей.

LaTeX

$$$\text{For } x \in X,\ NeBot(\mathcal{N}_{\ne}(x)) \Rightarrow NeBot(\mathcal{N}_{\ne}(x:\operatorname{OnePoint} X)).$$$

Lean4

/-- If `x` is not an isolated point of `X`, then `x : OnePoint X` is not an isolated point
of `OnePoint X`. -/
instance nhdsNE_coe_neBot (x : X) [h : NeBot (𝓝[≠] x)] : NeBot (𝓝[≠] (x : OnePoint X)) := by
  simpa [nhdsWithin_coe, preimage, coe_eq_coe] using h.map some

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