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

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
⊢ a ∈ thickening u s ↔ ∃ x ∈ s, (x, a) ∈ u
Tactic:
simp only [thickening, ball, mem_iUnion, mem_preimage, exists_prop]
State after:
no goals