log_lt_log

Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

URI: https://scilib.ai/kg/mathlib#ENNReal.log_lt_log

English

If x < y, then log x < log y.

Русский

Если x < y, то log x < log y.

LaTeX

$$$x < y \\implies \\log x < \\log y$$$

Lean4

@[gcongr]
theorem log_lt_log {x y : ℝ≥0∞} (h : x < y) : log x < log y :=
  log_strictMono h

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

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

Разделы

Аффилиация

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