hasStrictDerivAt — Mathlib

English

If f is C^n with n ≥ 1, then HasStrictDerivAt f (deriv f x) x.

Русский

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

LaTeX

$$$ContDiff At\\ 𝕂\\ n\\ f\\ x \\land 1 \\le n\\Rightarrow HasStrictDerivAt\\ f (deriv\\ f\\ x) x$$$

Lean4

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

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