pow_le_one_of_le

Mathlib.Algebra.Order.Monoid.Unbundled.Pow

URI: https://scilib.ai/kg/mathlib#Right.pow_le_one_of_le

English

If x ≤ 1, then x^n ≤ 1 for all n ∈ ℕ.

Русский

Если x ≤ 1, то x^n ≤ 1 для всех n ∈ ℕ.

LaTeX

$$$ x \le 1 \Rightarrow (\forall n \in \mathbb{N}, x^n \le 1) $$$

Lean4

@[to_additive Right.nsmul_nonpos]
theorem pow_le_one_of_le (hx : x ≤ 1) {n : ℕ} : x ^ n ≤ 1 :=
  Right.one_le_pow_of_le (M := Mᵒᵈ) hx

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru