log_lt_log_succ_iff — Mathlib

English

For base b > 1 and n > 0, log_b n < log_b (n+1) if and only if 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)} = n+1 $$$

Lean4

theorem log_lt_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
  refine ⟨fun H ↦ ?_, fun H ↦ ?_⟩
  · apply le_antisymm _ (Nat.lt_pow_of_log_lt hb H)
    exact Nat.pow_log_le_self b (Ne.symm (Nat.zero_ne_add_one n))
  · apply Nat.log_lt_of_lt_pow hn
    simp [H]

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