no goals
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : DiscreteTopology ↑s
x : α
hx : x ∈ s
⊢ ∃ U, U ∈ 𝓝 x ∧ U ∩ s = {x}
simpa using (𝓝 x).basis_sets.exists_inter_eq_singleton_of_mem_discrete hx