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