log_mono_right — Mathlib

English

For fixed base b, the log function is monotone in its argument on ordinals: if x ≤ y then log b x ≤ log b y.

Русский

При фиксированной основе b логарифм по аргументу возрастает: если x ≤ y, то log_b x ≤ log_b y.

LaTeX

$$$ x \le y \Rightarrow \log_b x \le \log_b y $$$

Lean4

@[mono]
theorem log_mono_right (b : Ordinal) {x y : Ordinal} (xy : x ≤ y) : log b x ≤ log b y :=
  by
  obtain rfl | hx := eq_or_ne x 0
  · simp_rw [log_zero_right, Ordinal.zero_le]
  · obtain hb | hb := lt_or_ge 1 b
    · exact (opow_le_iff_le_log hb (hx.bot_lt.trans_le xy).ne').1 <| (opow_log_le_self _ hx).trans xy
    · rw [log_of_left_le_one hb, log_of_left_le_one hb]

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