nhds_top' — Mathlib

English

A variant description: 𝓝 ∞ equals the infimum over a ≥ 0 of principal filters of Ioi (↑a).

Русский

Эквивалентное описание: 𝓝 ∞ равняется инфиминума над a ≥ 0 принципиальных фильтров Ioi (↑a).

LaTeX

$$$\\mathcal{N}(\\infty) = \\bigwedge_{a \\in \\mathbb{R}_{\\ge 0}} \\mathcal{P}(\\mathrm{Ioi}(\\uparrow a))$$$

Lean4

theorem nhds_top' : 𝓝 ∞ = ⨅ r : ℝ≥0, 𝓟 (Ioi ↑r) :=
  nhds_top.trans <| iInf_ne_top _

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