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 (⊥ : α)]