no goals
α : Type u
β : Type v
X : Type ?u.284548
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t : Set α
d : ℝ≥0∞
f : β → α
s : Set β
⊢ diam (f '' s) ≤ d ↔ ∀ (x : β), x ∈ s → ∀ (y : β), y ∈ s → edist (f x) (f y) ≤ d
simp only [diam_le_iff, ball_image_iff]