zpow_lt_iff_lt_clog — Mathlib

English

For base b>1 and r>0, (b^x) < r if and only if x < clog_b(r).

Русский

Для основания b>1 и r>0 верно: (b^x) < r тогда и только тогда x < clog_b(r).

LaTeX

$$$ (b^{x}) < r \iff x < \operatorname{clog}_b(r), \quad b>1, \ r>0 $$$

Lean4

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

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