zpow_le_iff_le_log — Mathlib

English

If x > 0 and y > 0, then x^n ≤ y iff n log x ≤ log y holds for all integers n.

Русский

Если x > 0 и y > 0, то для всех целых n выполняется x^n ≤ y тогда и только тогда, когда n log x ≤ log y.

LaTeX

$$$0 < x \land 0 < y \Rightarrow \forall n \in \mathbb{Z},\ x^n \le y \iff n \log x \le \log y$$$

Lean4

theorem zpow_le_iff_le_log {n : ℤ} (hx : 0 < x) (hy : 0 < y) : x ^ n ≤ y ↔ n * log x ≤ log y := by
  rw [← rpow_le_iff_le_log hx hy, rpow_intCast]

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