no goals
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : OrderTopology α
⊢ 𝓝 ⊥ = ⨅ (l : α) (_ : ⊥ < l), 𝓟 (Iio l)
simp [nhds_eq_order (⊥ : α)]