one_le_zpow

Mathlib.Algebra.Order.Monoid.Unbundled.Pow

URI: https://scilib.ai/kg/mathlib#one_le_zpow

← MathLib Explorer

English

For any n, under left-strict-mono, x^n < 1 ⇔ x < 1.

Русский

При левой строгой монотонности, для любого n: x^n < 1 ⇔ x < 1.

LaTeX

$$$\forall n\in\mathbb{N},\ (x^n < 1 \iff x < 1)$$$

Lean4

@[to_additive zsmul_nonneg]
theorem one_le_zpow {x : G} (H : 1 ≤ x) {n : ℤ} (hn : 0 ≤ n) : 1 ≤ x ^ n :=
  by
  lift n to ℕ using hn
  rw [zpow_natCast]
  apply one_le_pow_of_one_le' H

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

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

Разделы

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

Аффилиация

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