fderiv_exp — Mathlib

English

If f is differentiable at x, then the derivative of exp(f) at x is exp(f(x)) times the derivative of f at x.

Русский

Если f дифференцируема в x, то производная exp(f) в x равна exp(f(x)) умноженной на производную f в x.

LaTeX

$$$$ \text{DifferentiableAt}(f, x) \Rightarrow fderiv(\lambda y. \exp(f(y))) x = \exp(f(x)) \cdot fderiv f x $$$$

Lean4

@[simp]
theorem fderiv_exp (hc : DifferentiableAt ℝ f x) :
    fderiv ℝ (fun x => Real.exp (f x)) x = Real.exp (f x) • fderiv ℝ f x :=
  hc.hasFDerivAt.exp.fderiv

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