fderiv_eq — Mathlib

English

If a function has a power series at a point x, then its Fréchet derivative at x equals the first coefficient p(1) carried by the same curry operation to the target space.

Русский

Если функция имеет степенную серию в точке x, то её фредеховая производная в точке x равна первому коэффициенту p(1), приведённому аналогичным образом к целевому пространству.

LaTeX

$$$fderiv\\ f\\ x = \\operatorname{continuousMultilinearCurryFin1}_{\\mathbb{K}} E F (p\,1)$$$

Lean4

theorem fderiv_eq (h : HasFPowerSeriesAt f p x) : fderiv 𝕜 f x = continuousMultilinearCurryFin1 𝕜 E F (p 1) :=
  h.hasFDerivAt.fderiv

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