exp_hasFPowerSeriesOnBall — Mathlib

English

The exponential map has a full power-series expansion on the ball of convergence with radius ∞.

Русский

У экспоненциальной карты есть развёртывание в полный степенной ряд на шаре сходности с радиусом ∞.

LaTeX

$$$\text{HasFPowerSeriesOnBall } (\exp 𝕂) (\expSeries 𝕂 𝔸) 0 \infty$$$

Lean4

theorem exp_hasFPowerSeriesOnBall : HasFPowerSeriesOnBall (exp 𝕂) (expSeries 𝕂 𝔸) 0 ∞ :=
  expSeries_radius_eq_top 𝕂 𝔸 ▸ hasFPowerSeriesOnBall_exp_of_radius_pos (expSeries_radius_pos _ _)

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