exp

Mathlib.Analysis.SpecialFunctions.ExpDeriv

URI: https://scilib.ai/kg/mathlib#Differentiable.exp

English

If f is differentiable, then exp(f) is differentiable.

Русский

Если f дифференцируема, то exp(f) дифференцируема.

LaTeX

$$$$ \text{Differentiable}(f) \Rightarrow \text{Differentiable}(\lambda x. \exp(f(x))) $$$$

Lean4

@[simp, fun_prop]
theorem exp (hc : Differentiable ℝ f) : Differentiable ℝ fun x => Real.exp (f x) := fun x => (hc x).exp

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

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

Разделы

Аффилиация

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