hasFPowerSeriesOnBall_exp_of_radius_pos

English

Analogous HasSum statement for primed expansion.

Русский

Аналогичное утверждение о сумме для примированной экспоненты.

LaTeX

$$HasSum (fun n => ContinuousMultilinearMap.funLike.coe (expSeries 𝕂 𝔸 n) (fun x => x)) (NormedSpace.exp 𝕂 x)$$

Lean4

theorem hasFPowerSeriesOnBall_exp_of_radius_pos (h : 0 < (expSeries 𝕂 𝔸).radius) :
    HasFPowerSeriesOnBall (exp 𝕂) (expSeries 𝕂 𝔸) 0 (expSeries 𝕂 𝔸).radius :=
  (expSeries 𝕂 𝔸).hasFPowerSeriesOnBall h

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