inv_pow_lt_inv_pow_of_lt — Mathlib

English

For 1 < a, the inverse power a^n is strictly monotone in n.

Русский

Для 1 < a показатель a^n строго возрастает/уменьшается по n в зависимости от условия.

LaTeX

$$$1 < a \Rightarrow n < m \Rightarrow (a^{n})^{-1} > (a^{m})^{-1}$$$

Lean4

theorem inv_pow_lt_inv_pow_of_lt (a1 : 1 < a) {m n : ℕ} (mn : m < n) : (a ^ n)⁻¹ < (a ^ m)⁻¹ := by
  convert one_div_pow_lt_one_div_pow_of_lt a1 mn using 1 <;> simp

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