sinh_lt_cosh

Mathlib.Analysis.Complex.Trigonometric

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

English

For all real numbers x, sinh x is strictly less than cosh x.

Русский

Для любого действительного числа x выполняется неравенство sinh x < cosh x.

LaTeX

$$$\\\\forall x \in \\mathbb{R}, \\\\sinh x < \\\\cosh x$$$

Lean4

theorem sinh_lt_cosh : sinh x < cosh x :=
  lt_of_pow_lt_pow_left₀ 2 (cosh_pos _).le <| (cosh_sq x).symm ▸ lt_add_one _

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

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

Разделы

Аффилиация

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