hasDerivWithinAt_iff_isLittleO — Mathlib

English

HasDerivWithinAt f f' s x is equivalent to the IsLittleO condition with nhds within s at x: f x' - f x - (x' - x) f' = o_{𝓝[s] x}(x' - x).

Русский

HasDerivWithinAt f f' s x эквивалентно IsLittleO: разность изображений минус линейная аппроксимация пропорциональна (x' - x).

LaTeX

$$$\\mathrm{HasDerivWithinAt}(f,f',s,x) \\iff (f\\,x' - f\\,x - (x' - x) \\cdot f') =o_{\\mathcal{N}[s] x} (x' - x).$$$

Lean4

theorem hasDerivWithinAt_iff_isLittleO :
    HasDerivWithinAt f f' s x ↔ (fun x' : 𝕜 => f x' - f x - (x' - x) • f') =o[𝓝[s] x] fun x' => x' - x :=
  hasFDerivAtFilter_iff_isLittleO ..

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