pow_le_iff_le_log — Mathlib

English

If b > 1 and y ≠ 0, then b^x ≤ y iff x ≤ log_b y.

Русский

Пусть b > 1 и y ≠ 0. Тогда b^x ≤ y эквивалентно x ≤ log_b y.

LaTeX

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

Lean4

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

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