hasStrictFDerivAt — Mathlib

English

If f is C^n around x, then its Fréchet derivative at x is strict, i.e., HasStrictFDerivAt f (fderiv 𝕂 f x) x.

Русский

Если функция C^n в окрестности точки, то её Фрéше-дифференциал в этой точке является строгим.

LaTeX

$$$ContDiffAt\\ 𝕂\\ n\\ f\\ x \\land 1 \\le n\\Rightarrow HasStrictFDerivAt\\ f\\ (fderiv\\ 𝕂\\ f\\ x)\\ x$$$

Lean4

/-- If a function is `C^n` with `1 ≤ n` around a point, then the derivative of `f` at this point
is also a strict derivative. -/
theorem hasStrictFDerivAt {f : E' → F'} {x : E'} (hf : ContDiffAt 𝕂 n f x) (hn : 1 ≤ n) :
    HasStrictFDerivAt f (fderiv 𝕂 f x) x :=
  hf.hasStrictFDerivAt' (hf.differentiableAt hn).hasFDerivAt hn

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