hasDerivWithinAt_iff_tendsto — Mathlib

English

HasDerivAt f f' x is equivalent to IsLittleO with nhds x: f x' - f x - (x' - x) f' = o_{nhds x} (x' - x).

Русский

HasDerivAt эквивалентно IsLittleO: f x' - f x - (x' - x) f' = o_{nhds x} (x' - x).

LaTeX

$$$\\mathrm{HasDerivAt}(f,f',x) \\iff (f\\,x' - f\\,x - (x' - x) \\cdot f') =o_{\\mathcal{N} x} (x' - x).$$$

Lean4

theorem hasDerivWithinAt_iff_tendsto :
    HasDerivWithinAt f f' s x ↔ Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - (x' - x) • f'‖) (𝓝[s] x) (𝓝 0) :=
  hasFDerivAtFilter_iff_tendsto

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