clog_eq_clog_succ_iff — Mathlib

English

For base b > 1, clog_b n = clog_b(n+1) iff 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} \\neq n \\quad (1 < b) $$$

Lean4

theorem clog_eq_clog_succ_iff {b n : ℕ} (hb : 1 < b) : clog b n = clog b (n + 1) ↔ b ^ clog b n ≠ n :=
  by
  rw [ne_eq, ← clog_lt_clog_succ_iff hb, not_lt]
  simp only [le_antisymm_iff, and_iff_right_iff_imp]
  exact fun _ ↦ clog_monotone b (le_add_right n 1)

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