one_le_leOnePart

Mathlib.Algebra.Order.Group.PosPart

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

English

Let α be a lattice-ordered group and a ∈ α. Then the negative part a⁻ᵐ is also bounded below by 1, i.e. 1 ≤ a⁻ᵐ.

Русский

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

LaTeX

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

Lean4

@[to_additive negPart_nonneg]
theorem one_le_leOnePart (a : α) : 1 ≤ a⁻ᵐ :=
  le_sup_right

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

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

Разделы

Аффилиация

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