pow_lt_one_of_lt

Mathlib.Algebra.Order.Monoid.Unbundled.Pow

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

← MathLib Explorer

English

If 0 < n and x < 1, then x^n < 1.

Русский

Если 0 < n и x < 1, тогда x^n < 1.

LaTeX

$$$ n > 0 \land x < 1 \Rightarrow x^n < 1 $$$

Lean4

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

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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