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

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t : Set α
x u v : Set (α × α)
inst✝ : UniformSpace α
s : Set α
⊢ 𝓝ˢ s ≤ 𝓝ᵘ s
Tactic:
simpa [nhdsSet] using λ _ => nhds_le_uniform_nhds_set
State after:
no goals