leOnePart_le_one'

Mathlib.Algebra.Order.Group.PosPart

URI: https://scilib.ai/kg/mathlib#leOnePart_le_one'

← MathLib Explorer

English

In a lattice-ordered group, a⁻ᵐ ≤ 1 is equivalent to a⁻¹ ≤ 1.

Русский

В решёточно упорядоченной группе a⁻ᵐ ≤ 1 эквивалентно a⁻¹ ≤ 1.

LaTeX

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

Lean4

/-- See also `leOnePart_le_one`. -/
@[to_additive /-- See also `negPart_nonpos`. -/
    ]
theorem leOnePart_le_one' : a⁻ᵐ ≤ 1 ↔ a⁻¹ ≤ 1 := by simp [leOnePart]

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

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

Разделы

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

Аффилиация

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