nhds_top' — Mathlib

English

The neighborhood at the top is the infimum over all a ∈ ℝ of principal filters on Ioi a (the top neighborhood structure described via toEReal).

Русский

Окрестность в вершине ⊤ равна наименьшему элементу по фильтрам, полученным из Ioi a (a ∈ ℝ) через отображение toEReal.

LaTeX

$$$\\mathcal{N}(\\top) = \\bigwedge_{a\\in\\mathbb{R}} \\mathcal{P}(Ioi(a)^{\\mathrm{toEReal}})$$$

Lean4

theorem nhds_top' : 𝓝 (⊤ : EReal) = ⨅ a : ℝ, 𝓟 (Ioi ↑a) :=
  nhds_top_basis.eq_iInf

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