simpa [← uniform_nhds_set_singleton] using uniform_nhds_set_mono (singleton_subset_iff.mpr ha)
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t : Set α
x u v : Set (α × α)
inst✝ : UniformSpace α
s : Set α
ha : a ∈ s
⊢ 𝓝 a ≤ 𝓝ᵘ s
no goals