zpow_right_strictAnti₀ — Mathlib

English

Let a be an element of a group with zero such that 0 < a < 1. Then the function n ↦ a^n on the integers is strictly decreasing; equivalently, for all m,n ∈ ℤ with m < n we have a^m > a^n.

Русский

Пусть a принадлежит группе с нулём и 0 < a < 1. Тогда отображение n ↦ a^n из целых чисел в группу является строго убывающим; то есть для любых m,n ∈ ℤ при m < n имеет место a^m > a^n.

LaTeX

$$$0 < a < 1 \implies \forall m,n \in \mathbb{Z},\ m < n \implies a^{m} > a^{n}$$$

Lean4

theorem zpow_right_strictAnti₀ (ha₀ : 0 < a) (ha₁ : a < 1) : StrictAnti fun n : ℤ ↦ a ^ n :=
  by
  refine strictAnti_int_of_succ_lt fun n ↦ ?_
  rw [zpow_add_one₀ ha₀.ne']
  exact mul_lt_of_lt_one_right (zpow_pos ha₀ _) ha₁

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