pow_lt_iff_lt_clog — Mathlib

English

Let b > 1 be a natural number and x, y be natural numbers. Then b^y < x if and only if y < clog_b(x).

Русский

Пусть b > 1 — натуральное число, и x, y — натуральные числа. Тогда b^y < x тогда же, как и y < clog_b(x).

LaTeX

$$$ b^y < x \\iff y < \\operatorname{clog}_b x $$$

Lean4

@[deprecated lt_clog_iff_pow_lt (since := "2025-10-05")]
theorem pow_lt_iff_lt_clog {b : ℕ} (hb : 1 < b) {x y : ℕ} : b ^ y < x ↔ y < clog b x :=
  (lt_clog_iff_pow_lt hb).symm

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