hasStrictFDerivAt_id — Mathlib

English

For a strict Frechet derivative, the reverse big-O bound on the difference is established.

Русский

Для строгой производной Фреше установлено обратное big-O отношение для разности.

LaTeX

$$HasStrictFDerivAt f f' x → (fun p => p.1 - p.2) =O[nhds { fst := x, snd := x }] (fun p => f p.1 - f p.2)$$

Lean4

@[fun_prop]
theorem hasStrictFDerivAt_id (x : E) : HasStrictFDerivAt id (.id 𝕜 E) x :=
  .of_isLittleOTVS <| (IsLittleOTVS.zero _ _).congr_left <| by simp

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