self_le_sinh_iff

Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

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

← MathLib Explorer

English

For all real x, x ≤ sinh x iff 0 ≤ x.

Русский

Для любого x верно: x ≤ sinh x эквивалентно 0 ≤ x.

LaTeX

$$x \le \sinh x \iff 0 \le x$$

Lean4

@[simp]
theorem self_le_sinh_iff : x ≤ sinh x ↔ 0 ≤ x :=
  calc
    x ≤ sinh x ↔ sinh 0 - 0 ≤ sinh x - x := by simp
    _ ↔ 0 ≤ x := sinh_sub_id_strictMono.le_iff_le

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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