English
If f is differentiable at Rz, then L ∘ f ∘ R is differentiable at z.
Русский
Если f дифференцируемо в точке Rz, то L ∘ f ∘ R дифференцируемо в z.
LaTeX
$$$\mathrm{DifferentiableAt}_{\mathbb{K}} f (Rz) \Rightarrow \mathrm{DifferentiableAt}_{\mathbb{K}} (L \circ f \circ R) z$$$
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 : E → F} {f' : E →L[𝕜] F} {x₀ : E} (hf : HasFDerivAt f f' x₀) {s : Set E} (hs : s ∈ 𝓝 x₀)
{C : ℝ≥0} (hlip : LipschitzOnWith C f s) : ‖f'‖ ≤ C :=
by
refine hf.le_of_lip' C.coe_nonneg ?_
filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)
