no goals
α : Type u_1
t t₁ t₂ : TopologicalSpace α
s : Set α
inst✝ : TopologicalSpace α
⊢ DiscreteTopology α ↔ ∀ (x : α), {x} ∈ 𝓝 x
simp only [← singletons_open_iff_discrete, isOpen_iff_mem_nhds, mem_singleton_iff, forall_eq]