mulRightReflectLT_of_mulRightStrictMono

English

If a group is equipped with a linear order and every right multiplication is strictly increasing, then right translations reflect the strict order: a < b if and only if a·c < b·c for all a, b, c.

Русский

Если группа снабжена линейным порядком и правое умножение строго возрастает, то правые транспозиции отражают строгий порядок: для всех a, b, c выполнено a < b тогда и только тогда a·c < b·c.

LaTeX

$$$\forall a,b,c\in N\;\bigl(a < b \iff a \cdot c < b \cdot c\bigr)$$$

Lean4

@[to_additive]
theorem mulRightReflectLT_of_mulRightStrictMono [Group N] [LT N] [MulRightStrictMono N] : MulRightReflectLT N :=
  inferInstance

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