exp — Mathlib

English

If f is ContDiff (Real) n, then x ↦ exp(f(x)) is ContDiff (Real) n.

Русский

Если f ∈ ContDiff ℝ n, то exp(f) ∈ ContDiff ℝ n.

LaTeX

$$$ \forall {E} [\text{NormedAddCommGroup } E] [\text{NormedSpace } \mathbb{R} E] \; {f:\, E\to \mathbb{R}} \;{n}:= \operatorname{WithTop} ℕ_\infty, \; \operatorname{ContDiff}_{\mathbb{R}} n f \Rightarrow \operatorname{ContDiff}_{\mathbb{R}} n (\lambda x, \exp(f(x)))$$$

Lean4

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

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