le_zpow_iff_clog_le — Mathlib

English

For base b>1 and r>0, r ≤ b^x iff clog_b(r) ≤ x.

Русский

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

LaTeX

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

Lean4

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

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