le_pow_sup

Mathlib.Algebra.Order.Monoid.Unbundled.Pow

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

English

In a lattice-ordered monoid with left/right monotone multiplication, (a ∧ b)^n ≤ a^n ∧ b^n.

Русский

В моноиде с порядком решётки и слева/справа монотонными умножениями, (a ∧ b)^n ≤ a^n ∧ b^n.

LaTeX

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

Lean4

theorem le_pow_sup : a ^ n ⊔ b ^ n ≤ (a ⊔ b) ^ n :=
  sup_le (pow_le_pow_left' le_sup_left _) (pow_le_pow_left' le_sup_right _)

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

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

Разделы

Аффилиация

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