exp — Mathlib

English

If f is differentiable within at x on s, then exp(f) is differentiable within at x on s.

Русский

Если f дифференцируема внутри множества s в точке x, то exp(f) дифференцируема внутри s в x.

LaTeX

$$$$ \text{DifferentiableWithinAt}_{\mathbb{R}}(f, s, x) \Rightarrow \text{DifferentiableWithinAt}_{\mathbb{R}}(\lambda y. \exp(f(y)), s, x) $$$$

Lean4

theorem exp (hf : DifferentiableWithinAt ℝ f s x) : DifferentiableWithinAt ℝ (fun x => Real.exp (f x)) s x :=
  hf.hasFDerivWithinAt.exp.differentiableWithinAt

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