Theorem: UniformSpace.uniform_nhds_set_singleton (RMT4/uniform.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
a✝ : α
s t : Set α
x u v : Set (α × α)
inst✝ : UniformSpace α
a : α
⊢ 𝓝ᵘ {a} = 𝓝 a
Tactic:
simp only [uniform_nhds_set, thickening_singleton, nhds_eq_uniformity]
State after:
no goals