zero_eq' — Mathlib

English

If f has a Taylor series up to order n with p, then for each x, p x 0 equals the symmetric curry of f(x): p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (f x).

Русский

Если функция f имеет разложение Тейлора до порядка n с p, то для каждого x коэффициент нулевого порядка равен соответствующему образу f(x) через естественное билинейное соответствие: p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (f x).

LaTeX

$$$p x 0 = (\text{continuousMultilinearCurryFin0 } 𝕜 E F).symm (f x)$$$

Lean4

theorem zero_eq' (h : HasFTaylorSeriesUpTo n f p) (x : E) : p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (f x) :=
  by
  rw [← h.zero_eq x]
  exact (p x 0).uncurry0_curry0.symm

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