contDiff_arsinh — Mathlib

English

Arsinh has ContDiff of all orders; in particular, it is infinitely differentiable.

Русский

Функция arsinh имеет гладкость ContDiff всех порядков; следовательно, она бесконечно дифференцируема.

LaTeX

$$$\\operatorname{ContDiff}_{\\mathbb{R}}^{n}(\\operatorname{arsinh}) \\\\text{for all } n \\in \\mathbb{N}_\\infty.$$$

Lean4

@[fun_prop]
theorem contDiff_arsinh {n : ℕ∞} : ContDiff ℝ n arsinh :=
  sinhHomeomorph.contDiff_symm_deriv (fun x => (cosh_pos x).ne') hasDerivAt_sinh contDiff_sinh

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