norm_deriv_le_of_lipschitz — Mathlib

English

If f is Lipschitz with constant C, then ||deriv f x0|| ≤ C.

Русский

Если f липшицева с константой C, тогда ||deriv f x0|| ≤ C.

LaTeX

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

Lean4

/-- Converse to the mean value inequality: if `f` is `C`-lipschitz then
its derivative at `x₀` has norm bounded by `C`.
Version using `deriv`. -/
theorem norm_deriv_le_of_lipschitz {f : 𝕜 → F} {x₀ : 𝕜} {C : ℝ≥0} (hlip : LipschitzWith C f) : ‖deriv f x₀‖ ≤ C := by
  simpa [norm_deriv_eq_norm_fderiv] using norm_fderiv_le_of_lipschitz 𝕜 hlip

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