toPosSMulReflectLT — Mathlib

English

Let R be a ordered semiring and M an ordered additive monoid with an R-action. Then positivity of scalars reflects strict order: if a > 0 and a • x < a • y, then x < y.

Русский

Пусть R — упорядоченная полугруппа и M — упорядоченная аддитивная моноида с действием R на M. Тогда если a > 0 и a • x < a • y, то x < y.

LaTeX

$$$ \forall R M \,[\text{Semiring } R], [\text{PartialOrder } R], [\text{AddCommMonoid } M], [\text{PartialOrder } M], [\text{SMulWithZero } R M], [\text{OrderedSMul } R M],\quad \forall a\ x\ y,\ 0 < a \rightarrow a \cdot x < a \cdot y \rightarrow x < y. $$$

Lean4

instance toPosSMulReflectLT : PosSMulReflectLT R M :=
  .of_pos fun _a ha _b₁ _b₂ h ↦ OrderedSMul.lt_of_smul_lt_smul_of_pos h ha

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