mulRightStrictMono_of_mulRightReflectLE

English

If a semigroup is linear-ordered and left reflect LE, then right multiplication is strictly monotone.

Русский

Если полугруппа линейно упорядочена и выполняется отражение LE слева, правая умножение строго монотонна.

LaTeX

$$$\text{RightStrictMono}$ holds under $\text{LeftReflectLE}$ in a linear-ordered semigroup.$$

Lean4

@[to_additive]
theorem mulRightStrictMono_of_mulRightReflectLE [Mul N] [LinearOrder N] [MulRightReflectLE N] : MulRightStrictMono N :=
  inferInstance

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