no goals
𝓕 : Type ?u.185016
𝕜 : Type ?u.185019
α : Type ?u.185022
ι : Type ?u.185025
κ : Type ?u.185028
E : Type u_1
F : Type u_2
G : Type ?u.185037
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : E → F
C : ℝ≥0
⊢ LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x / f y‖ ≤ ↑C * ‖x / y‖
simp only [lipschitzOnWith_iff_dist_le_mul, dist_eq_norm_div]