exp — Mathlib

English

If f has a Fréchet derivative f' within a set s at x, then exp(f) has derivative exp(f(x)) times f' within s at x.

Русский

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

LaTeX

$$$$ \HasFDerivWithinAt(f, f', s, x) \Rightarrow \HasFDerivWithinAt(\lambda y. \exp(f(y)), \exp(f(x)) \cdot f', s, x) $$$$

Lean4

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

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