log_eq_log_succ_iff — Mathlib

English

For base b > 1 and n > 0, log_b n = log_b(n+1) iff b^{log_b(n+1)} ≠ n+1.

Русский

Для основания b > 1 и n > 0 верно: log_b n = log_b(n+1) тогда и только тогда, когда b^{log_b(n+1)} ≠ n+1.

LaTeX

$$$ (1 < b) \land (n \neq 0) \Rightarrow \log_b n = \log_b(n+1) \iff b^{\log_b(n+1)} \neq n+1 $$$

Lean4

theorem log_eq_log_succ_iff {b n : ℕ} (hb : 1 < b) (hn : n ≠ 0) : log b n = log b (n + 1) ↔ b ^ log b (n + 1) ≠ n + 1 :=
  by
  rw [ne_eq, ← log_lt_log_succ_iff hb hn, not_lt]
  simp only [le_antisymm_iff, and_iff_right_iff_imp]
  exact fun _ ↦ log_monotone (le_add_right n 1)

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