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