toPosSMulReflectLT — Mathlib

English

In the same setting as above, multiplication by a positive scalar reflects strict 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.

Русский

В той же постановке положительная скаляра отражает строгий порядок: если a > 0 и b1 < b2, то a•b1 < a•b2, и наоборот.

LaTeX

$$$ \forall a>0,\; b_1,b_2:\ G,\; b_1 < b_2 \iff a\cdot b_1 < a\cdot b_2 $$$

Lean4

instance (priority := 100) toPosSMulReflectLT [MulActionWithZero 𝕜 G] [PosSMulStrictMono 𝕜 G] : PosSMulReflectLT 𝕜 G :=
  .of_pos fun a ha b₁ b₂ h ↦ by simpa [ha.ne'] using smul_lt_smul_of_pos_left h <| inv_pos.2 ha

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