hasDerivAt_iff_tendsto — Mathlib

English

HasDerivAt f f' x is equivalent to a Tendsto condition of the same normalized error to 0 with nhds x.

Русский

HasDerivAt эквивалентно условию сходимости того же нормированного остатка к нулю при x.

LaTeX

$$$\\mathrm{HasDerivAt}(f,f',x) \\iff \\mathrm{Tendsto}\\left( \\lambda x' \\;\\mapsto\\; \\|x' - x\\|^{-1} \\cdot \\|f x' - f x - (x' - x) \\cdot f'\\| \\right) (\\mathcal{N} x) (\\mathcal{N} 0\\,).$$$

Lean4

theorem hasDerivAt_iff_tendsto :
    HasDerivAt f f' x ↔ Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - (x' - x) • f'‖) (𝓝 x) (𝓝 0) :=
  hasFDerivAtFilter_iff_tendsto

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