HasStrictDerivAt — Mathlib

English

The function f has a strict derivative at x with slope f' if the limit definition of strict differentiability holds; i.e., HasStrictDerivAt f f' x.

Русский

Функция f имеет строгую производную в точке x с касательной f'.

LaTeX

$$$\\text{HasStrictDerivAt}(f,f',x).$$$

Lean4

/-- `f` has the derivative `f'` at the point `x` in the sense of strict differentiability.

That is, `f y - f z = (y - z) • f' + o(y - z)` as `y, z → x`. -/
def HasStrictDerivAt (f : 𝕜 → F) (f' : F) (x : 𝕜) :=
  HasStrictFDerivAt f (smulRight (1 : 𝕜 →L[𝕜] 𝕜) f') x

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