cosh_strictMonoOn

Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

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

← MathLib Explorer

English

Let f(x) = cosh x. Then f is strictly increasing on [0, ∞).

Русский

Пусть f(x) = cosh x. Функция cosh строго возрастает на [0, ∞).

LaTeX

$$$\\forall x,y\\ge 0,\\ x

Lean4

theorem cosh_strictMonoOn : StrictMonoOn cosh (Ici 0) :=
  strictMonoOn_of_deriv_pos (convex_Ici _) continuous_cosh.continuousOn fun x hx => by rw [interior_Ici, mem_Ioi] at hx;
    rwa [deriv_cosh, sinh_pos_iff]

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

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

Разделы

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

Аффилиация

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