no goals
ι : Sort ?u.21870
α : Type ?u.21873
β : Type ?u.21876
X : Type u_1
Y : Type ?u.21882
inst✝ : TopologicalSpace X
x : X
⊢ 𝓝 (𝓝 x) = ⨅ (s : Set X) (_ : IsOpen s) (_ : x ∈ s), 𝓟 (Iic (𝓟 s))
simp only [(nhds_basis_opens x).nhds.eq_biInf, iInf_and, @iInf_comm _ (_ ∈ _)]