clog_anti_left — Mathlib

English

For any n, and for hc: 1 < c and hb: c ≤ b, clog_b(n) ≤ clog_c(n).

Русский

Для любых n и для hc: 1 < c, hb: c ≤ b, выполняется clog_b(n) ≤ clog_c(n).

LaTeX

$$$ (1 < c) \\land (c \\le b) \\implies \\operatorname{clog}_b n \\le \\operatorname{clog}_c n $$$

Lean4

theorem clog_anti_left {b c n : ℕ} (hc : 1 < c) (hb : c ≤ b) : clog b n ≤ clog c n :=
  by
  rw [clog_le_iff_le_pow (lt_of_lt_of_le hc hb)]
  calc
    n ≤ c ^ clog c n := le_pow_clog hc _
    _ ≤ b ^ clog c n := Nat.pow_le_pow_left hb _

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