zpow_right_mono — Mathlib

English

If 1 ≤ a in a commutative group with a partial order and IsOrderedMonoid, then the map n ↦ a^n is monotone.

Русский

Если 1 ≤ a в коммутативной группе с порядком и IsOrderedMonoid, то функция n ↦ a^n монотонна.

LaTeX

$$$ [CommGroup \\alpha] [PartialOrder \\alpha] [IsOrderedMonoid \\alpha] {a : \\alpha}, 1 \\le a \\Rightarrow \\text{Monotone}(n \\mapsto a^n). $$$

Lean4

@[to_additive zsmul_left_mono]
theorem zpow_right_mono (ha : 1 ≤ a) : Monotone fun n : ℤ ↦ a ^ n :=
  by
  refine monotone_int_of_le_succ fun n ↦ ?_
  rw [zpow_add_one]
  exact le_mul_of_one_le_right' ha

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