logb_le_logb_of_le

Mathlib.Analysis.SpecialFunctions.Log.Base

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

English

If b > 1 and 0 < x ≤ y, then log_b x ≤ log_b y.

Русский

Если b > 1 и 0 < x ≤ y, тогда log_b x ≤ log_b y.

LaTeX

$$$1 < b \land 0 < x \land x \le y \Rightarrow \log_b x \le \log_b y.$$$

Lean4

@[gcongr]
theorem logb_le_logb_of_le (h : 0 < x) (hxy : x ≤ y) : logb b x ≤ logb b y :=
  (logb_le_logb hb h (by linarith)).mpr hxy

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

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

Разделы

Аффилиация

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