no goals
α : Type u
β : Type v
ι : Type ?u.17404
π : ι → Type ?u.17409
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
l : Filter α
hs : IsCompact s
⊢ Disjoint l (𝓝ˢ s) ↔ ∀ (x : α), x ∈ s → Disjoint l (𝓝 x)
simpa only [disjoint_comm] using hs.disjoint_nhdsSet_left