zero_eq' — Mathlib

English

If h : HasFTaylorSeriesUpToOn n f p s and x ∈ s, then p x 0 equals the evaluation of f at x under the currying correspondence.

Русский

Если h : HasFTaylorSeriesUpToOn n f p s и x ∈ s, то p x 0 равно значению f x через корректное соответствие карриинга.

LaTeX

$$$HasFTaylorSeriesUpToOn\ n\ f\ p\ s \to {x} \in s\Rightarrow p x 0 = (\text{continuousMultilinearCurryFin0 } 𝕜 E F)^{-1} (f x)$$$

Lean4

theorem zero_eq' (h : HasFTaylorSeriesUpToOn n f p s) {x : E} (hx : x ∈ s) :
    p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (f x) :=
  by
  rw [← h.zero_eq x hx]
  exact (p x 0).uncurry0_curry0.symm

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