log_le_log

Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

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

English

If x ≤ y, then log x ≤ log y.

Русский

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

LaTeX

$$$x \\le y \\implies \\log x \\le \\log y$$$

Lean4

@[gcongr]
theorem log_le_log {x y : ℝ≥0∞} (h : x ≤ y) : log x ≤ log y :=
  log_monotone h

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

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

Разделы

Аффилиация

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