norm_div_le_of_le — Mathlib

English

If f is Lipschitz on a set s, for a, b ∈ s, and ‖a/b‖ ≤ r, then ‖f(a)/f(b)‖ ≤ C⋅r.

Русский

Если f Lipschitz на множестве s, для a,b ∈ s и ‖a/b‖ ≤ r, то ‖f(a)/f(b)‖ ≤ C⋅r.

LaTeX

$$$\\text{If } f\\text{ is LipschitzOnWith } C\\ f\\ s,\\ ha, hb \\in s,\\ ||a/b|| ≤ r \\implies ||f(a)/f(b)|| ≤ C \\cdot r$$$

Lean4

@[to_additive]
theorem norm_div_le_of_le {f : E → F} {C : ℝ≥0} (h : LipschitzOnWith C f s) (ha : a ∈ s) (hb : b ∈ s)
    (hr : ‖a / b‖ ≤ r) : ‖f a / f b‖ ≤ C * r :=
  (h.norm_div_le ha hb).trans <| by gcongr

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