cexp

Mathlib.Analysis.SpecialFunctions.ExpDeriv

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

English

If f is differentiable on a set s, then exp ∘ f is differentiable on s.

Русский

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

LaTeX

$$$ \\forall s,\\text{DifferentiableOn }(\\exp \\circ f) s = \\text{DifferentiableOn } f s$$$

Lean4

theorem cexp (hc : DifferentiableOn 𝕜 f s) : DifferentiableOn 𝕜 (fun x => Complex.exp (f x)) s := fun x h =>
  (hc x h).cexp

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

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

Разделы

Аффилиация

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