English
The identity map id is differentiable (simplicity, standard fact).
Русский
Идентичность id дифференцируема (классическая простая теорема).
LaTeX
$$$\mathrm{Differentiable}_{\mathbb{K}}(\mathrm{id})$$$
Lean4
/-- Converse to the mean value inequality: if `f` is `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 norm_fderiv_le_of_lip' {f : E → F} {x₀ : E} {C : ℝ} (hC₀ : 0 ≤ C)
(hlip : ∀ᶠ x in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖) : ‖fderiv 𝕜 f x₀‖ ≤ C :=
by
by_cases hf : DifferentiableAt 𝕜 f x₀
· exact hf.hasFDerivAt.le_of_lip' hC₀ hlip
· rw [fderiv_zero_of_not_differentiableAt hf]
simp [hC₀]
