hasFPowerSeriesAt_exp_zero_of_radius_pos

English

If radius is positive, then exp has a power series on that ball with radius equal to expSeries.radius.

Русский

Если радиус положителен, то у экспоненты есть степенной ряд на шаре с радиусом expSeries.radius.

LaTeX

$$HasFPowerSeriesOnBall (exp 𝕂) (expSeries 𝕂 𝔸) 0 (expSeries 𝕂 𝔸).radius$$

Lean4

theorem hasFPowerSeriesAt_exp_zero_of_radius_pos (h : 0 < (expSeries 𝕂 𝔸).radius) :
    HasFPowerSeriesAt (exp 𝕂) (expSeries 𝕂 𝔸) 0 :=
  (hasFPowerSeriesOnBall_exp_of_radius_pos h).hasFPowerSeriesAt

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