contDiff_cosh

Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

URI: https://scilib.ai/kg/mathlib#Real.contDiff_cosh

English

Cosh is ContDiff of every order; in particular, it is smooth and analytic.

Русский

Cosh является contDiff для любого порядка; следовательно, гладок и аналитичен.

LaTeX

$$$\forall n \in \mathrm{WithTop}\; \mathbb{ENat},\; \mathrm{ContDiff}_{\mathbb{R}}(n, \cosh)$$$

Lean4

@[fun_prop]
theorem contDiff_cosh {n} : ContDiff ℝ n cosh :=
  Complex.contDiff_cosh.real_of_complex

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru