continuousOn_exp

Mathlib.Analysis.Normed.Algebra.Exponential

URI: https://scilib.ai/kg/mathlib#NormedSpace.continuousOn_exp

English

There exists a HasFPowerSeriesAt for exp at 0 when the radius is positive.

Русский

Существует HasFPowerSeriesAt для exp в точке 0 при положительном радиусе.

LaTeX

$$HasFPowerSeriesAt (exp 𝕂) (expSeries 𝕂 𝔸) 0$$

Lean4

theorem continuousOn_exp : ContinuousOn (exp 𝕂 : 𝔸 → 𝔸) (EMetric.ball 0 (expSeries 𝕂 𝔸).radius) :=
  FormalMultilinearSeries.continuousOn

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru