pow_le_one_of_le — Mathlib

English

Let M be a monoid with a compatible preorder and MulRightMono. If a ≤ 1, then a^n ≤ 1 for every n ∈ ℕ.

Русский

Пусть имеется моноид M с совместимым порядком и правая монотонность умножения. Если a ≤ 1, то a^n ≤ 1 для всех n ∈ ℕ.

LaTeX

$$a \le 1 ⇒ ∀ n ∈ ℕ, a^n ≤ 1$$

Lean4

@[to_additive nsmul_nonpos]
theorem pow_le_one_of_le (ha : a ≤ 1) (n : ℕ) : a ^ n ≤ 1 :=
  one_le_pow_of_le (M := Mᵒᵈ) ha n

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