no goals
α : Type u_1
β : Type ?u.8534
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ Disjoint (𝓝ˢ s) (𝓟 t) ↔ Disjoint s (closure t)
rw [disjoint_comm, disjoint_principal_nhdsSet, disjoint_comm]