no goals
α : Type u_1
β : Type ?u.11427
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ 𝓝ˢ s = 𝓟 s ↔ IsOpen s
rw [← principal_le_nhdsSet.le_iff_eq, le_principal_iff, mem_nhdsSet_iff_forall,
  isOpen_iff_mem_nhds]