hasStrictFDerivAt — Mathlib

English

If f is C^n for some n ≥ 1, then f has a strict Fréchet derivative at x with value fderiv 𝕂 f x.

Русский

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

LaTeX

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

Lean4

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

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