le_of_lipschitz — Mathlib

English

If f is Lipschitz with constant C, then the norm of its derivative at x0 is bounded by C.

Русский

Если f липшицева с константой C, то норма производной в x0 ограничена C.

LaTeX

$$$\\|\\operatorname{deriv}f(x_0)\\| \\le C$ for LipshitzWith C f$$

Lean4

/-- Converse to the mean value inequality: if `f` is differentiable at `x₀` and `C`-lipschitz
then its derivative at `x₀` has norm bounded by `C`. -/
theorem le_of_lipschitz {f : 𝕜 → F} {f' : F} {x₀ : 𝕜} (hf : HasDerivAt f f' x₀) {C : ℝ≥0} (hlip : LipschitzWith C f) :
    ‖f'‖ ≤ C := by simpa using HasFDerivAt.le_of_lipschitz hf.hasFDerivAt hlip

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