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

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
⊢ Disjoint (ball a u) t ↔ ∀ b ∈ t, (a, b) ∉ u
Tactic:
rw [← compl_compl (ball a u), disjoint_compl_left_iff_subset]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
⊢ t ⊆ (ball a u)ᶜ ↔ ∀ b ∈ t, (a, b) ∉ u

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
⊢ t ⊆ (ball a u)ᶜ ↔ ∀ b ∈ t, (a, b) ∉ u
Tactic:
rfl
State after:
no goals