le_oneLePart

Mathlib.Algebra.Order.Group.PosPart

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

English

For every a in a lattice-ordered group, the original element is bounded above by its positive part: a ≤ a⁺ᵐ.

Русский

Для каждого a в решёточно упорядоченной группе имеет место неравенство: a ≤ a⁺ᵐ.

LaTeX

$$$a \le a^{+m}$$$

Lean4

@[to_additive le_posPart]
theorem le_oneLePart (a : α) : a ≤ a⁺ᵐ :=
  le_sup_left

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

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

Разделы

Аффилиация

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