HasDerivAt — Mathlib

English

The derivative of f at x, if it exists, is denoted deriv f x; otherwise it is zero by convention.

Русский

Производная функции f в точке x обозначается как deriv f x; если производной нет, она равна нулю по условию.

LaTeX

$$$\\mathrm{deriv}(f,x) = fderiv\\ 𝕜\\ f\\ x\\ 1$$$

Lean4

/-- `f` has the derivative `f'` at the point `x`.

That is, `f x' = f x + (x' - x) • f' + o(x' - x)` where `x'` converges to `x`.
-/
def HasDerivAt (f : 𝕜 → F) (f' : F) (x : 𝕜) :=
  HasDerivAtFilter f f' x (𝓝 x)

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