exp — Mathlib

English

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

Русский

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

LaTeX

$$$ \text{HasStrictDerivAt}_{\mathbb{R}} (\exp \circ f) (\exp(f(x)) \cdot f') x$$$

Lean4

theorem exp (hf : HasStrictDerivAt f f' x) : HasStrictDerivAt (fun x => Real.exp (f x)) (Real.exp (f x) * f') x :=
  (Real.hasStrictDerivAt_exp (f x)).comp x hf

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