derivWithin_exp — Mathlib

English

If f is differentiable within s at x, and s has a unique differentiability point at x, then derivWithin exp(f) s x = exp(f(x))·derivWithin f s x.

Русский

Если f дифференцируема внутри s в x и x является уникальной точкой дифференцирования, то derivWithin(exp(f)) = exp(f(x))·derivWithin f.

LaTeX

$$$ \operatorname{derivWithin}_{s} (\lambda x, \exp(f(x))) x = \exp(f(x)) \cdot \operatorname{derivWithin}_{s} f x$$$

Lean4

theorem derivWithin_exp (hf : DifferentiableWithinAt ℝ f s x) (hxs : UniqueDiffWithinAt ℝ s x) :
    derivWithin (fun x => Real.exp (f x)) s x = Real.exp (f x) * derivWithin f s x :=
  hf.hasDerivWithinAt.exp.derivWithin hxs

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