exp — Mathlib

English

Let E be a normed space over R and f: E → R. If f is ContDiffAt of order n at x, then the function x ↦ exp(f(x)) is ContDiffAt of order n at x.

Русский

Пусть E — нормированное пространство над R и f: E → R. Если f ∈ ContDiffAt n в точке x, то x ↦ exp(f(x)) ∈ ContDiffAt n в точке x.

LaTeX

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

Lean4

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

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