nhds_eq_pure — Mathlib

English

For ENat values other than top, the neighborhood filter equals the pure filter.

Русский

Для значений ENat, отличных от верхнего, окрестностной фильтр совпадает с чистым фильтром.

LaTeX

$$$$\\forall n \\in \\mathbb{N}_{\\infty},\\; n \\neq \\top \\Rightarrow \\mathcal{N}(n) = \\operatorname{pure}(n).$$$$

Lean4

@[simp]
protected theorem nhds_eq_pure {n : ℕ∞} (h : n ≠ ⊤) : 𝓝 n = pure n :=
  by
  lift n to ℕ using h
  simp [nhds_natCast]

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