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

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
⊢ thickening u s ∩ t = ∅ ↔ ∀ a ∈ s, ∀ b ∈ t, (a, b) ∉ u
Tactic:
simp [thickening, ← disjoint_iff_inter_eq_empty, disjoint_ball_iff]
State after:
no goals