nhds_bot_order — Mathlib

English

Dual to the top-case: the neighborhood of the bottom element is the infimum over l with ⊥ < l of principal filters of Iio l.

Русский

Двойственность к верхнему случаю: окрестности нуля равны инфиминуму по l с ⊥ < l их простым фильтрам Iio l.

LaTeX

$$$\\mathcal{N}(\\bot) = \\bigwedge_{l>\\bot} \\mathcal{P}(Iio(l)).$$$

Lean4

theorem nhds_bot_order [TopologicalSpace α] [Preorder α] [OrderBot α] [OrderTopology α] :
    𝓝 (⊥ : α) = ⨅ (l) (_ : ⊥ < l), 𝓟 (Iio l) := by simp [nhds_eq_order (⊥ : α)]

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