contDiff_sinh — Mathlib

English

The function sinh is infinitely differentiable on the complex plane; in fact, it is analytic of all orders.

Русский

Функция sinh бесконечно дифференцируема на плоскости комплексных чисел; она аналитична во всех порядках.

LaTeX

$$$\operatorname{ContDiff}_{\mathbb{C}} n\;\sinh \quad\text{for all } n$$$

Lean4

@[fun_prop]
theorem contDiff_sinh {n} : ContDiff ℂ n sinh :=
  (contDiff_exp.sub contDiff_neg.cexp).div_const _

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