fpowerSeries_apply_zero — Mathlib

English

The zero-th coefficient of fpowerSeries is the uncurry-0 evaluation of f at x.

Русский

Нулевой коэффициент fpowerSeries равен uncurry0 применения f к x.

LaTeX

$$$ fpowerSeries\\_apply\\_zero (f : E \\to L[𝕜] F) (x : E) : fpowerSeries x 0 = ContinuousMultilinearMap.uncurry0 𝕜 E (f x) $$$

Lean4

@[simp]
theorem fpowerSeries_apply_zero (f : E →L[𝕜] F) (x : E) :
    f.fpowerSeries x 0 = ContinuousMultilinearMap.uncurry0 𝕜 _ (f x) :=
  rfl

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