exp_sub_sinh

Mathlib.Analysis.Complex.Trigonometric

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

English

For all real x, exp x - sinh x = cosh x.

Русский

Для всех x: exp x - sinh x = cosh x.

LaTeX

$$$\\exp x - \\sinh x = \\cosh x$$$

Lean4

@[simp]
theorem exp_sub_sinh : exp x - sinh x = cosh x :=
  sub_eq_iff_eq_add.2 (cosh_add_sinh x).symm

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

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

Разделы

Аффилиация

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