clog_lt_clog_succ_iff — Mathlib

English

For base b > 1, clog_b n < clog_b(n+1) if and only if b^{clog_b n} = n.

Русский

Для основания b > 1 выполняется clog_b n < clog_b(n+1) тогда же, как и b^{clog_b n} = n.

LaTeX

$$$ \\operatorname{clog}_b n < \\operatorname{clog}_b(n+1) \\iff b^{\\operatorname{clog}_b n} = n \\quad (1 < b) $$$

Lean4

theorem clog_lt_clog_succ_iff {b n : ℕ} (hb : 1 < b) : clog b n < clog b (n + 1) ↔ b ^ clog b n = n :=
  by
  refine ⟨fun H ↦ ?_, fun H ↦ ?_⟩
  · apply le_antisymm _ (le_pow_clog hb n)
    apply le_of_lt_succ
    exact (lt_clog_iff_pow_lt hb).mp H
  · rw [lt_clog_iff_pow_lt hb, H]
    exact n.lt_add_one

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