nhds_top — Mathlib

English

The neighborhood filter at ∞ in ENNReal is the infimum of principal filters of rays Ioi a for a ≠ ∞.

Русский

Окрестностная фильтрация в ∞ в ENNReal есть наименьшее пересечение простых фильтров по лучам Ioi a при a ≠ ∞.

LaTeX

$$$\\mathcal{N}(\\infty) = \\bigwedge_{a \\neq \\infty} \\mathcal{P}(\\mathrm{Ioi}\\, a)$$$

Lean4

theorem nhds_top : 𝓝 ∞ = ⨅ (a) (_ : a ≠ ∞), 𝓟 (Ioi a) :=
  nhds_top_order.trans <| by simp [lt_top_iff_ne_top, Ioi]

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