hasFPowerSeriesOnBall_const — Mathlib

English

A constant map x ↦ c has a formal power series expansion on any ball around any point, given by the constant multilinear series.

Русский

Константная функция x ↦ c имеет формальный степенной ряд на любом шаре вокруг любой точки, задаваемый постоянной многообразной серией.

LaTeX

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

Lean4

theorem hasFPowerSeriesOnBall_const {c : F} {e : E} :
    HasFPowerSeriesOnBall (fun _ => c) (constFormalMultilinearSeries 𝕜 E c) e ⊤ :=
  by
  refine ⟨by simp, WithTop.top_pos, fun _ => hasSum_single 0 fun n hn => ?_⟩
  simp [constFormalMultilinearSeries_apply_of_nonzero hn]

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