sinh — Mathlib

English

If a function f is n-times continuously differentiable (ContDiff ℝ n), then the composition with the hyperbolic sine is again n-times continuously differentiable: x ↦ sinh(f(x)) is ContDiff ℝ n.

Русский

Если функция f является n-раз непрерывно дифференцируемой, то композиция sinh ∘ f тоже является n-раз непрерывно дифференцируемой: x ↦ sinh(f(x)).

LaTeX

$$$\operatorname{ContDiff}_{\mathbb{R}}^{n}(f) \Rightarrow \operatorname{ContDiff}_{\mathbb{R}}^{n}( \sinh \circ f ).$$$

Lean4

theorem sinh {n} (h : ContDiff ℝ n f) : ContDiff ℝ n fun x => Real.sinh (f x) :=
  Real.contDiff_sinh.comp h

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