nhds_top — Mathlib

English

The topology at the top element ⊤ in EReal is the infimum of principal filters of open upper rays Ioi a (a ∈ ℝ).

Русский

Топология в вершине ⊤ в EReal является наименьшей среди стандартных фильтров, задаваемых открытыми лучами Ioi a (a ∈ ℝ).

LaTeX

$$$\\mathcal{N}(\\top) = \\bigwedge_{a} \\mathcal{P}(Ioi(a))$$$

Lean4

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

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