sinh_strictMono

Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

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

English

The function sinh is strictly increasing on the real line.

Русский

Функция sinh строго возрастает на всей оси действительных чисел.

LaTeX

$$$\text{StrictMono}(\sinh)$$$

Lean4

/-- `sinh` is strictly monotone. -/
theorem sinh_strictMono : StrictMono sinh :=
  strictMono_of_deriv_pos <| by rw [Real.deriv_sinh]; exact cosh_pos

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

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

Разделы

Аффилиация

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