no goals
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
ha : ∃ l, l < a
⊢ 𝓝[Iic a] a = ⨅ (l : α) (_ : l < a), 𝓟 (Ioc l a)
simp only [nhdsWithin_Iic_eq'', biInf_inf ha, inf_principal, Ioi_inter_Iic]