le_of_lipschitz — Mathlib

English

For a bilinear map b that is bounded, differentiability at a point p implies differentiability at p.

Русский

Для ограниченной билинейной карты b дифференцируемость в точке p следует из дифференцируемости в p.

LaTeX

$$$\mathrm{DifferentiableAt}_{\mathbb{K}} b p$$$

Lean4

/-- Converse to the mean value inequality: if `f` is differentiable at `x₀` and `C`-lipschitz
then its derivative at `x₀` has norm bounded by `C`. -/
theorem le_of_lipschitz {f : E → F} {f' : E →L[𝕜] F} {x₀ : E} (hf : HasFDerivAt f f' x₀) {C : ℝ≥0}
    (hlip : LipschitzWith C f) : ‖f'‖ ≤ C :=
  hf.le_of_lipschitzOn univ_mem (lipschitzOnWith_univ.2 hlip)

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