log_mul_base — Mathlib

English

If y ≠ 0 and y < b^x then log_b y < x.

Русский

Если y ≠ 0 и y < b^x, тогда log_b y < x.

LaTeX

$$$\\forall {b,x,y} \\in \\mathbb{N}, \\; y \\neq 0 \\Rightarrow (y < b^x \\Rightarrow \\log_b y < x)$$$

Lean4

@[simp]
theorem log_mul_base {b n : ℕ} (hb : 1 < b) (hn : n ≠ 0) : log b (n * b) = log b n + 1 :=
  by
  apply log_eq_of_pow_le_of_lt_pow <;> rw [pow_succ', Nat.mul_comm b]
  exacts [Nat.mul_le_mul_right _ (pow_log_le_self _ hn),
    (Nat.mul_lt_mul_right (Nat.zero_lt_one.trans hb)).2 (lt_pow_succ_log_self hb _)]

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