no goals
α : Type u_2
β : Type u_1
inst✝ : EDist α
x y : α
s✝ t : Set α
d : ℝ≥0∞
f : β → α
s : Set β
⊢ d ≤ einfsep (f '' s) ↔ ∀ (x : β), x ∈ s → ∀ (y : β), y ∈ s → f x ≠ f y → d ≤ edist (f x) (f y)
simp_rw [le_einfsep_iff, ball_image_iff]