English
If f is C-Lipschitz with constant C and f is differentiable at x0 with derivative f', then ||f'|| ≤ C.
Русский
Если f является C-липшицевой функцией и имеет производную в x0, то ||f'|| ≤ C.
LaTeX
$$$\\|f'\\| \\le C \\quad \\text{whenever } \\text{HasDerivAt } f f' x_0 \\text{ and } f \\text{ is } C\\text{-Lipschitz}$$$
Lean4
/-- Converse to the mean value inequality: if `f` is differentiable at `x₀` and `C`-lipschitz
on a neighborhood of `x₀` then its derivative at `x₀` has norm bounded by `C`. -/
theorem le_of_lipschitzOn {f : 𝕜 → F} {f' : F} {x₀ : 𝕜} (hf : HasDerivAt f f' x₀) {s : Set 𝕜} (hs : s ∈ 𝓝 x₀) {C : ℝ≥0}
(hlip : LipschitzOnWith C f s) : ‖f'‖ ≤ C := by simpa using HasFDerivAt.le_of_lipschitzOn hf.hasFDerivAt hs hlip
