hasGradientAt_iff_isLittleO — Mathlib

English

hasGradientWithinAt_iff_isLittleO: HasGradientWithinAt f f' s x iff the IsLittleO condition holds with nhdsWithin.

Русский

Условие Малого О для градиента внутри множества s в точке x эквивалентно схеме nhdsWithin.

LaTeX

$$$\\text{HasGradientWithinAt } f f' s x \\iff \\IsLittleO_{\\ nhdsWithin x s}\\ (f(x')-f(x)-⟪f',x'-x⟫)\\ (x'-x)$$$

Lean4

theorem hasGradientAt_iff_isLittleO :
    HasGradientAt f f' x ↔ (fun x' : F => f x' - f x - ⟪f', x' - x⟫) =o[𝓝 x] fun x' => x' - x :=
  hasGradientAtFilter_iff_isLittleO

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