no goals
α : Type u
β : Type v
X : Type ?u.34183
ι : Type ?u.34186
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
⊢ closedBall x ε = ∅ ↔ ε < 0
rw [← not_nonempty_iff_eq_empty, nonempty_closedBall, not_le]