one_le_oneLePart

Mathlib.Algebra.Order.Group.PosPart

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

English

Let α be a lattice-ordered group and a ∈ α. Then the positive part a⁺ᵐ is at least the unit element, i.e. 1 ≤ a⁺ᵐ.

Русский

Пусть α — решёточно упорядоченная группа и a ∈ α. Тогда положительная часть a⁺ᵐ не меньше единицы: 1 ≤ a⁺ᵐ.

LaTeX

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

Lean4

@[to_additive posPart_nonneg]
theorem one_le_oneLePart (a : α) : 1 ≤ a⁺ᵐ :=
  le_sup_right

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

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

Разделы

Аффилиация

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