no goals
α : Type u
β : Type v
X : Type ?u.222978
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
⊢ (∀ (i : ℝ≥0∞), 0 < i → ∃ y, y ∈ s ∧ y ∈ ball x i) ↔ ∀ (ε : ℝ≥0∞), ε > 0 → ∃ y, y ∈ s ∧ edist x y < ε
simp only [mem_ball, edist_comm x]