hasStrictDerivAt — Mathlib

English

If f is C^n around x with n ≥ 1, then f has a strict derivative equal to its usual derivative at x.

Русский

Если функция C^n около точки и n ≥ 1, то производная есть строгая производная и равна обычной производной в точке.

LaTeX

$$$ContDiffAt\\ 𝕂\\ n\\ f\\ x \\land 1 \\le n\\Rightarrow HasStrictDerivAt\\ f\\ (deriv\\ 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 hasStrictDerivAt {f : 𝕂 → F'} {x : 𝕂} (hf : ContDiffAt 𝕂 n f x) (hn : 1 ≤ n) :
    HasStrictDerivAt f (deriv f x) x :=
  (hf.hasStrictFDerivAt hn).hasStrictDerivAt

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