zpow_right_strictMono₀ — Mathlib

English

If 1 < a, then n ↦ a^n is StrictMono on ℤ.

Русский

Если 1 < a, то n ↦ a^n строго монотонна по n на целых числах.

LaTeX

$$$$1 < a \Rightarrow \text{StrictMono}(n \mapsto a^{n}): \mathbb{Z} \to G_0.$$$$

Lean4

theorem zpow_right_strictMono₀ (ha : 1 < a) : StrictMono fun n : ℤ ↦ a ^ n :=
  by
  refine strictMono_int_of_lt_succ fun n ↦ ?_
  rw [zpow_add_one₀ (zero_lt_one.trans ha).ne']
  exact lt_mul_of_one_lt_right (zpow_pos (zero_lt_one.trans ha) _) ha

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