exp — Mathlib

English

If f is ContDiffWithinAt n on s at x, then exp ∘ f is ContDiffWithinAt n on s at x.

Русский

Если f ∈ ContDiffWithinAt n на s в точке x, то exp ∘ f ∈ ContDiffWithinAt n на s в x.

LaTeX

$$$$ \operatorname{ContDiffWithinAt}_{\mathbb{R}}(n, f, s, x) \Rightarrow \operatorname{ContDiffWithinAt}_{\mathbb{R}}(n, \lambda y. \exp(f(y)), s, x) $$$$

Lean4

@[fun_prop]
theorem exp {n} (hf : ContDiffWithinAt ℝ n f s x) : ContDiffWithinAt ℝ n (fun x => Real.exp (f x)) s x :=
  Real.contDiff_exp.contDiffAt.comp_contDiffWithinAt x hf

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