hasDerivAtFilter_iff_isLittleO — Mathlib

English

HasDerivAtFilter f f' x L is equivalent to the little-o condition: f x' - f x - (x' - x) f' is o_L (x' - x).

Русский

HasDerivAtFilter эквивалентно условию IsLittleO: f x' - f x - (x' - x) f' = o_L (x' - x).

LaTeX

$$$\\mathrm{HasDerivAtFilter}(f,f',x,L) \\iff (f\\,x' - f\\,x - (x' - x)\\,f') =o_L (x' - x).$$$

Lean4

theorem hasDerivAtFilter_iff_isLittleO :
    HasDerivAtFilter f f' x L ↔ (fun x' : 𝕜 => f x' - f x - (x' - x) • f') =o[L] fun x' => x' - x :=
  hasFDerivAtFilter_iff_isLittleO ..

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