clog_of_two_le — Mathlib

English

If hb: 1 < b and hn: 2 ≤ n, then clog_b(n) = clog_b((n + b − 1)/b) + 1.

Русский

Если hb: 1 < b и hn: 2 ≤ n, то clog_b(n) = clog_b((n + b − 1)/b) + 1.

LaTeX

$$$ (1 < b) \land (2 \le n) \Rightarrow \operatorname{clog}(b,n) = \operatorname{clog}\left(b, \frac{n + b - 1}{b}\right) + 1 $$$

Lean4

theorem clog_of_two_le {b n : ℕ} (hb : 1 < b) (hn : 2 ≤ n) : clog b n = clog b ((n + b - 1) / b) + 1 := by
  rw [clog, dif_pos (⟨hb, hn⟩ : 1 < b ∧ 1 < n)]

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