contDiff_exp

Mathlib.Analysis.SpecialFunctions.ExpDeriv

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

English

For the real line, the exponential function is ContDiff of all orders n.

Русский

На вещественной линии экспонента имеет гладкость во всех порядках.

LaTeX

$$$ \forall n, \operatorname{ContDiff}_{\mathbb{R}} n \exp$$$

Lean4

@[fun_prop]
theorem contDiff_exp {n : WithTop ℕ∞} : ContDiff ℝ n exp :=
  Complex.contDiff_exp.real_of_complex

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

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

Разделы

Аффилиация

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