deriv — Mathlib

English

For any f and x and s, HasDerivWithinAt f f' s x is equivalent to HasFDerivWithinAt f (f' 1) s x.

Русский

Для любой функции f и точек x и множества s, HasDerivWithinAt f f' s x эквивалентно HasFDerivWithinAt f (f' 1) s x.

LaTeX

$$$\\text{HasDerivWithinAt}(f,f',s,x) \\iff \\text{HasFDerivWithinAt}(f,f',s,x).$$$

Lean4

/-- Derivative of `f` at the point `x`, if it exists.  Zero otherwise.

If the derivative exists (i.e., `∃ f', HasDerivAt f f' x`), then
`f x' = f x + (x' - x) • deriv f x + o(x' - x)` where `x'` converges to `x`.
-/
def deriv (f : 𝕜 → F) (x : 𝕜) :=
  fderiv 𝕜 f x 1

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