∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedCommGroup E] [inst_1 : SeminormedCommGroup F] {f : E → F} {C : NNReal}
  {s : Set E} {a b : E} {r : ℝ}, LipschitzOnWith C f s → a ∈ s → b ∈ s → ‖a / b‖ ≤ r → ‖f a / f b‖ ≤ ↑C * r