nhds_top_order — Mathlib

English

In a topological ordered space with OrderTopology, the neighborhood of the top element is the infimum of principal neighborhoods generated by Ioi(l) as l ranges below the top.

Русский

В топологическом упорядоченном пространстве с OrderTopology окрестности максимального элемента — это инфиминум над окрестностями, порождаемыми Ioi(l) при l < ⊤.

LaTeX

$$$\\mathcal{N}(\\top) = \\bigwedge_{l<\\top} \\mathcal{P}(Ioi(l)).$$$

Lean4

theorem nhds_top_order [TopologicalSpace α] [Preorder α] [OrderTop α] [OrderTopology α] :
    𝓝 (⊤ : α) = ⨅ (l) (_ : l < ⊤), 𝓟 (Ioi l) := by simp [nhds_eq_order (⊤ : α)]

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