no goals
α✝ : Type u
β : Type v
ι : Sort w
a✝ : α✝
s s₁ s₂ t : Set α✝
p p₁ p₂ : α✝ → Prop
inst✝¹ : TopologicalSpace α✝
α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ IsOpen {a} ↔ 𝓝[{a}ᶜ] a = ⊥
rw [isOpen_singleton_iff_nhds_eq_pure, nhdsWithin, ← mem_iff_inf_principal_compl, ← le_pure_iff,
  nhds_neBot.le_pure_iff]