no goals
α : Type u
β : Type v
γ : Type ?u.13446
δ : Type ?u.13449
ε : Type ?u.13452
ζ : Type ?u.13455
inst✝ : TopologicalSpace α
S : Set α
⊢ DiscreteTopology ↑S ↔ ∀ (x : α), x ∈ S → 𝓝[{x}ᶜ] x ⊓ 𝓟 S = ⊥
simp_rw [discreteTopology_iff_nhds_ne, SetCoe.forall', nhds_ne_subtype_eq_bot_iff]