no goals
α : Type u_1
t t₁ t₂ : TopologicalSpace α
s : Set α
inst✝ : TopologicalSpace α
⊢ DiscreteTopology α ↔ ∀ (x : α), 𝓝[{x}ᶜ] x = ⊥
simp only [discreteTopology_iff_singleton_mem_nhds, nhdsWithin, inf_principal_eq_bot, compl_compl]