English
If f is Lipschitz on a neighborhood of x0 with constant C, then the norm of its derivative at x0 is at most C.
Русский
Если f является C-липшицевой на окрестности x0 с константой C, то нормa производной в x0 не превышает C.
LaTeX
$$$\\|\\operatorname{deriv}f(x_0)\\| \\le C \\quad \\text{whenever } s \\in \\mathcal{N}(x_0) \\text{ and } f\\text{ is LipshitzOnWith } C\\ f\\ s$$$
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`. This version
only assumes that `‖f x - f x₀‖ ≤ C * ‖x - x₀‖` in a neighborhood of `x`. -/
theorem le_of_lip' {f : 𝕜 → F} {f' : F} {x₀ : 𝕜} (hf : HasDerivAt f f' x₀) {C : ℝ} (hC₀ : 0 ≤ C)
(hlip : ∀ᶠ x in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖) : ‖f'‖ ≤ C := by
simpa using HasFDerivAt.le_of_lip' hf.hasFDerivAt hC₀ hlip
