English
Under an ordered field 𝕜 and an ordered additive group G with a linear action of 𝕜, the positive scalar action preserves and reflects the order: if a > 0 and b1 ≤ b2, then a • b1 ≤ a • b2, and conversely, if a > 0 and a • b1 ≤ a • b2, then b1 ≤ b2.
Русский
При наличии упорядоченного поля 𝕜 и упорядоченной аддитивной группы G с действием 𝕜 на G положительный скаляльный множитель сохраняет порядок и отражает его: если a > 0 и b1 ≤ b2, то a • b1 ≤ a • b2, и наоборот, если a > 0 и a • b1 ≤ a • b2, то b1 ≤ b2.
LaTeX
$$$ \forall a>0,\; b_1,b_2:\ G,\; b_1 \le b_2 \iff a\cdot b_1 \le a\cdot b_2 $$$
Lean4
instance (priority := 100) toPosSMulReflectLE [MulAction 𝕜 G] [PosSMulMono 𝕜 G] : PosSMulReflectLE 𝕜 G where
le_of_smul_le_smul_left _a ha b₁ b₂ h := by simpa [ha.ne'] using smul_le_smul_of_nonneg_left h <| inv_nonneg.2 ha.le
