English
If f is differentiable within s at x and x is a unique differentiable point within s, then fderivWithin of exp(f) on s at x equals exp(f(x)) times fderivWithin f on s at x.
Русский
Если f дифференцируема внутри s в x и x является уникальной точкой дифференцирования внутри s, тогда fderivWithin( exp(f) ) s x = exp(f(x)) · fderivWithin f s x.
LaTeX
$$$$ \text{DifferentiableWithinAt}(f, s, x) \land \text{UniqueDiffWithinAt}(s, x) \Rightarrow fderivWithin \mathbb{R}(\lambda y. \exp(f(y))) s x = \exp(f(x)) \cdot fderivWithin \mathbb{R} f s x $$$$
Lean4
theorem fderivWithin_exp (hf : DifferentiableWithinAt ℝ f s x) (hxs : UniqueDiffWithinAt ℝ s x) :
fderivWithin ℝ (fun x => Real.exp (f x)) s x = Real.exp (f x) • fderivWithin ℝ f s x :=
hf.hasFDerivWithinAt.exp.fderivWithin hxs
