zpow_right_strictAnti — Mathlib

English

If a < 1 in a commutative group with a partial order and IsOrderedMonoid, then the map n ↦ a^n is strictly anti-monotone on ℤ.

Русский

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

LaTeX

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

Lean4

@[to_additive zsmul_left_strictAnti]
theorem zpow_right_strictAnti (ha : a < 1) : StrictAnti fun n : ℤ ↦ a ^ n :=
  by
  refine strictAnti_int_of_succ_lt fun n ↦ ?_
  rw [zpow_add_one]
  exact mul_lt_of_lt_one_right' (a ^ n) ha

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