cexp — Mathlib

English

If f has a strict derivative f' at x, then exp(f(x)) has strict derivative exp(f(x))·f' at x.

Русский

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

LaTeX

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

Lean4

theorem cexp (hf : HasFDerivWithinAt f f' s x) :
    HasFDerivWithinAt (fun x => Complex.exp (f x)) (Complex.exp (f x) • f') s x :=
  (Complex.hasDerivAt_exp (f x)).comp_hasFDerivWithinAt x hf

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