one_le_pow_iff

Mathlib.Algebra.Order.Monoid.Unbundled.Pow

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

← MathLib Explorer

English

In a semilattice-sup Monoid, a^n ⊔ b^n ≤ (a ⊔ b)^n.

Русский

В моноиде с верхой (супом) степеней: a^n ⊔ b^n ≤ (a ⊔ b)^n.

LaTeX

$$$ a^n \lor b^n \le (a \lor b)^n $$$

Lean4

@[to_additive nsmul_nonneg_iff]
theorem one_le_pow_iff {x : M} {n : ℕ} (hn : n ≠ 0) : 1 ≤ x ^ n ↔ 1 ≤ x :=
  ⟨le_imp_le_of_lt_imp_lt fun h => pow_lt_one' h hn, fun h => one_le_pow_of_one_le' h n⟩

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

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

Разделы

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

Аффилиация

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