deriv_exp — Mathlib

English

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

Русский

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

LaTeX

$$$ \text{If } \text{DifferentiableAt}_{\mathbb{R}} f x, \; \dfrac{d}{dx} \exp(f(x)) = \exp(f(x)) \cdot f'(x)$$$

Lean4

@[simp]
theorem deriv_exp (hc : DifferentiableAt ℝ f x) : deriv (fun x => Real.exp (f x)) x = Real.exp (f x) * deriv f x :=
  hc.hasDerivAt.exp.deriv

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