Theorem: UniformSpace.mem_uniform_nhds_set_iff (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 ∈ 𝓝ᵘ t ↔ ∃ u ∈ 𝓤 α, thickening u t ⊆ s
Tactic:
simp [uniform_nhds_set, mem_lift'_sets]
State after:
no goals