hasFPowerSeriesAt_const — Mathlib

English

For a constant function x ↦ c there is a formal power series expansion about every point e with coefficients given by the same constant multilinear series.

Русский

Для константной функции вокруг любой точки e существует формальный степенной ряд с коэффициентами, задаваемыми той же константной многообразной серией.

LaTeX

$$$HasFPowerSeriesAt(\\lambda x. c,\\; constFormalMultilinearSeries_{\\mathbb{k}}(E,c),\\ e)$$$

Lean4

theorem hasFPowerSeriesAt_const {c : F} {e : E} :
    HasFPowerSeriesAt (fun _ => c) (constFormalMultilinearSeries 𝕜 E c) e :=
  ⟨⊤, hasFPowerSeriesOnBall_const⟩

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