lt_zpow_iff_log_lt — Mathlib

English

For base b > 1 and any r > 0, r < b^x iff log_b(r) < x. This is the standard tightness of the log-base-b relation.

Русский

Для основания b > 1 и любого r > 0 верно: r < b^x тогда log_b(r) < x; эквивалентность мгновенной точности связи логарифма и степени.

LaTeX

$$$r > 0 \Rightarrow (r < b^x) \;\Leftrightarrow\; (\log_b r) < x$$$

Lean4

/-- `zpow b` and `Int.log b` (almost) form a Galois connection. -/
theorem lt_zpow_iff_log_lt {b : ℕ} (hb : 1 < b) {x : ℤ} {r : R} (hr : 0 < r) : r < (b : R) ^ x ↔ log b r < x :=
  @GaloisConnection.lt_iff_lt _ _ _ _ _ _ (zpowLogGi R hb).gc x ⟨r, hr⟩

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