toSMulPosStrictMono — Mathlib

English

Multiplication by a positive element on the right is strictly monotone: if b1 < b2 and a > 0, then b1·a < b2·a.

Русский

Умножение слева или справа положительным элементом по отношению к правому аргументу сохраняет строгое монотонное изменение.

LaTeX

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

Lean4

instance (priority := 100) toSMulPosStrictMono [MulPosStrictMono α] : SMulPosStrictMono α α where
  smul_lt_smul_of_pos_right _b hb _a₁ _a₂ ha := mul_lt_mul_of_pos_right ha hb

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