lt_pow_iff_log_lt — Mathlib

English

For base b > 1 and y > 0, y < b^x iff log_b y < x.

Русский

Для основания b > 1 и y > 0 верно: y < b^x тогда log_b y < x.

LaTeX

$$$\\forall b \\in \\mathbb{N}, \\; 1 < b \\land y \\in \\mathbb{N}, y \\neq 0 \\Rightarrow \\; y < b^x \\iff \\log_b y < x$$$

Lean4

@[deprecated log_lt_iff_lt_pow (since := "2025-10-05")]
theorem lt_pow_iff_log_lt {b : ℕ} (hb : 1 < b) {x y : ℕ} (hy : y ≠ 0) : y < b ^ x ↔ log b y < x :=
  (log_lt_iff_lt_pow hb hy).symm

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