toSMulPosReflectLT — Mathlib

English

Multiplication by a positive element on the left yields a relation that mirrors the order: if a>0 and b1 < b2, then a·b1 < a·b2.

Русский

Умножение слева на положительный элемент сохраняет порядок: если a>0 и b1 < b2, то a·b1 < a·b2.

LaTeX

$$$a>0 \\land b_1 < b_2 \\Rightarrow a\\cdot b_1 < a\\cdot b_2.$$$

Lean4

instance (priority := 100) toSMulPosReflectLT [MulPosReflectLT α] : SMulPosReflectLT α α where
  lt_of_smul_lt_smul_right _b hb _a₁ _a₂ h := lt_of_mul_lt_mul_right h hb

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