lipschitzWith_iff_norm_div_le — Mathlib

English

LipschitzWith C f is equivalent to the inequality ‖f x/f y‖ ≤ C⋅‖x/y‖ for all x,y.

Русский

Липшицевость эквивалентна неравенству ‖f(x)/f(y)‖ ≤ C⋅‖x/y‖ для всех x,y.

LaTeX

$$$\\text{LipschitzWith } C f \\iff \\forall x,y,\\ \\|f(x)/f(y)\\| ≤ C·\\|x/y\\|$$$

Lean4

@[to_additive]
theorem lipschitzWith_iff_norm_div_le {f : E → F} {C : ℝ≥0} : LipschitzWith C f ↔ ∀ x y, ‖f x / f y‖ ≤ C * ‖x / y‖ := by
  simp only [lipschitzWith_iff_dist_le_mul, dist_eq_norm_div]

Похожие утверждения