exp — Mathlib

English

Let E be a normed space over R and f: E → R. If f is ContDiffOn n on a set s, then exp( f ) is ContDiffOn n on s.

Русский

Пусть E — нормированное пространство над R и f: E → R. Если f ∈ ContDiffOn n на множество s, то exp ∘ f ∈ ContDiffOn n на s.

LaTeX

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

Lean4

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

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