hasStrictFDerivAt_iff_isLittleO — Mathlib

English

Same equivalence as above but in a doubled form over the product space with nhds.

Русский

Та же эквивалентность для произведённого пространства с фильтром nhds.

LaTeX

$$$\text{HasStrictFDerivAt } f f' x \iff \text{IsLittleO } (nhds\{ fst:=x, snd:=x \}) (f p.fst - f p.snd - f'(p.fst-p.snd)) (p.fst-p.snd)$$$

Lean4

theorem hasStrictFDerivAt_iff_isLittleO :
    HasStrictFDerivAt f f' x ↔
      (fun p : E × E => f p.1 - f p.2 - f' (p.1 - p.2)) =o[𝓝 (x, x)] fun p : E × E => p.1 - p.2 :=
  (hasStrictFDerivAt_iff_isLittleOTVS ..).trans isLittleOTVS_iff_isLittleO

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