leOnePart_lt

Mathlib.Algebra.Order.Group.PosPart

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

English

In a linear-ordered group with left and right monotonicity, leOnePart LT is a consequence of pos/neg-part relations.

Русский

В линейно упорядоченной группе с левой и правой монотонностью следует из relation частей.

LaTeX

$$leOnePart_lt$$

Lean4

@[to_additive (attr := simp)]
theorem leOnePart_lt : a⁻ᵐ < b ↔ b⁻¹ < a ∧ 1 < b :=
  sup_lt_iff.trans <| by rw [inv_lt']

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

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

Разделы

Аффилиация

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