no goals
α : Type u
β : Type v
X : Type ?u.25922
ι : Type ?u.25925
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
⊢ ball x ε = ∅ ↔ ε ≤ 0
rw [← not_nonempty_iff_eq_empty, nonempty_ball, not_lt]