contDiff_exp

Mathlib.Analysis.SpecialFunctions.ExpDeriv

URI: https://scilib.ai/kg/mathlib#Complex.contDiff_exp

English

The exponential is ContDiff of all orders; in particular it is C^∞.

Русский

Экспонента бесконечно дифференцируема; она гладкая (C^∞).

LaTeX

$$$ \\forall n,\\; \\operatorname{ContDiff}_{\\mathbb{C}}(n, \\exp)$$$

Lean4

@[fun_prop]
theorem contDiff_exp {n : WithTop ℕ∞} : ContDiff 𝕜 n exp :=
  analyticOnNhd_cexp.restrictScalars.contDiff

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

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

Разделы

Аффилиация

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