nhdsNE_infty_neBot — Mathlib

English

If X is noncompact, then ∞ in OnePoint X is not an isolated point, i.e., 𝓝[≠]∞ is nontrivial.

Русский

Если X не компактно, то ∞ в OnePoint X не изолирована: 𝓝[≠]∞ не тождественно пусто.

LaTeX

$$$\text{instance } nhdsNE_infty_neBot [NoncompactSpace X] : NeBot (\mathcal{N}_{\ne} (\infty : OnePoint X)).$$$

Lean4

/-- If `X` is a non-compact space, then `∞` is not an isolated point of `OnePoint X`. -/
instance nhdsNE_infty_neBot [NoncompactSpace X] : NeBot (𝓝[≠] (∞ : OnePoint X)) :=
  by
  rw [nhdsNE_infty_eq]
  infer_instance

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