no goals
α : Type u_1
t t₁ t₂ : TopologicalSpace α
s : Set α
inst✝ : TopologicalSpace α
⊢ DiscreteTopology α ↔ ∀ (x : α), 𝓝 x = pure x
simp only [discreteTopology_iff_singleton_mem_nhds, ← nhds_neBot.le_pure_iff, le_pure_iff]