pow_lt_one_of_lt — Mathlib

English

Let M be a monoid with a preorder in which left multiplication is monotone. If a < 1 and n ≠ 0, then a^n < 1.

Русский

Пусть M — моноид с порядком, совместимым с умножением слева. Если a < 1 и n ≠ 0, то a^n < 1.

LaTeX

$$$ a < 1 \land n \ge 1 \Rightarrow a^n < 1 $$$

Lean4

@[to_additive nsmul_neg]
theorem pow_lt_one_of_lt {a : M} {n : ℕ} (h : a < 1) (hn : n ≠ 0) : a ^ n < 1 :=
  by
  rcases Nat.exists_eq_succ_of_ne_zero hn with ⟨k, rfl⟩
  rw [pow_succ']
  exact mul_lt_one_of_lt_of_le h (pow_le_one_of_le h.le _)

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