no goals
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : RegularSpace α
a✝ : α
s : Set α
a b : α
⊢ Disjoint (𝓝 a) (𝓝 b) ↔ ¬a ⤳ b
rw [← nhdsSet_singleton, disjoint_nhdsSet_nhds, specializes_iff_mem_closure]