clog_mono_right — Mathlib

English

For fixed b, if n ≤ m then clog_b(n) ≤ clog_b(m).

Русский

Для фиксированного b, если n ≤ m, то clog_b(n) ≤ clog_b(m).

LaTeX

$$$ n \\le m \\implies \\operatorname{clog}_b n \\le \\operatorname{clog}_b m $$$

Lean4

@[mono, gcongr]
theorem clog_mono_right (b : ℕ) {n m : ℕ} (h : n ≤ m) : clog b n ≤ clog b m :=
  by
  rcases le_or_gt b 1 with hb | hb
  · rw [clog_of_left_le_one hb]
    exact zero_le _
  · rw [clog_le_iff_le_pow hb]
    exact h.trans (le_pow_clog hb _)

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