hasStrictDerivAt' — Mathlib

English

If a function is C^n around a point and its derivative at that point is f', then f' is a strict derivative at that point.

Русский

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

LaTeX

$$$ContDiffAt\\ 𝕂\\ n\\ f\\ x \\land HasDerivAt\\ f\\ f'\\ x \\land 1 \\le n\\Rightarrow HasStrictDerivAt\\ f\\ f'\\ x$$$

Lean4

/-- If a function is `C^n` with `1 ≤ n` around a point, and its derivative at that point is given to
us as `f'`, then `f'` is also a strict derivative. -/
theorem hasStrictDerivAt' {f : 𝕂 → F'} {f' : F'} {x : 𝕂} (hf : ContDiffAt 𝕂 n f x) (hf' : HasDerivAt f f' x)
    (hn : 1 ≤ n) : HasStrictDerivAt f f' x :=
  hf.hasStrictFDerivAt' hf' hn

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