zpow_le_iff_le_log — Mathlib

English

For base b > 1 and r > 0, (b^x ≤ r) iff x ≤ log_b(r). This is the dual of the previous relation.

Русский

Пусть b > 1 и r > 0. Тогда b^x ≤ r эквивалентно x ≤ log_b(r).

LaTeX

$$$(b^x \le r) \Leftrightarrow (x \le \log_b r)$, для r>0$$

Lean4

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

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