cpolynomialAt — Mathlib

English

For a continuous linear map f, the zero-th coefficient in its power-series expansion at x exists and is the constant polynomial cpolynomialAt 𝕜 f x.

Русский

Для непрерывного линейного отображения f существует нулевой коэффициент в разложении в рядов Taylor вокруг точки x; этот коэффициент равен cpolynomialAt 𝕜 f x.

LaTeX

$$$ \mathrm{cpolynomialAt}_{\mathbb{k}} f x \in \text{CPolynomialAt } 𝕜 f x $$$

Lean4

protected theorem cpolynomialAt (f : E →L[𝕜] F) (x : E) : CPolynomialAt 𝕜 f x :=
  (f.hasFiniteFPowerSeriesOnBall x).cpolynomialAt

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