cexp

Mathlib.Analysis.SpecialFunctions.ExpDeriv

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

English

If f is differentiable at x, then exp ∘ f is differentiable at x.

Русский

Если f дифференцируема в x, то exp ∘ f дифференцируема в x.

LaTeX

$$$ \\forall x, \\text{DifferentiableAt}(\\exp \\circ f, x)$$$

Lean4

@[simp, fun_prop]
theorem cexp (hc : Differentiable 𝕜 f) : Differentiable 𝕜 fun x => Complex.exp (f x) := fun x => (hc x).cexp

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

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

Разделы

Аффилиация

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