self_lt_sinh_iff

Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

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

English

x < sinh x iff 0 < x.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem self_lt_sinh_iff : x < sinh x ↔ 0 < x :=
  lt_iff_lt_of_le_iff_le sinh_le_self_iff

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

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

Разделы

Аффилиация

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