sinh_lt_self_iff

Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

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

English

sinh x < x iff x < 0.

Русский

sinh x < x эквивалентно x < 0.

LaTeX

$$\\sinh x < x \\iff x < 0$$

Lean4

@[simp]
theorem sinh_lt_self_iff : sinh x < x ↔ x < 0 :=
  lt_iff_lt_of_le_iff_le self_le_sinh_iff

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

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

Разделы

Аффилиация

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