cexp — Mathlib

English

If f has a derivative at x with derivative f', then the derivative of exp(f(x)) at x is exp(f(x))·f'.

Русский

Если у f в точке x есть производная f', то производная exp(f(x)) в x равна exp(f(x))·f'.

LaTeX

$$$ \\forall x,\\ HasDerivAt f f' x \\Rightarrow HasDerivAt(\\exp \\circ f) (\\exp( f(x) ) \\cdot f') x$$$

Lean4

theorem cexp (hf : HasDerivAt f f' x) : HasDerivAt (fun x => Complex.exp (f x)) (Complex.exp (f x) * f') x :=
  (Complex.hasDerivAt_exp (f x)).comp x hf

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