cmp_mul_right' — Mathlib

English

Similarly, right-multiplication by a fixed element preserves the order of comparisons in a linear order when monotone on the right.

Русский

Аналогично, правое умножение сохраняет порядок сравнений в линейном порядке при монотонности справа.

LaTeX

$$$\forall a,b,c,\;cmp(a\cdot c, b\cdot c) = cmp(a,b)$$$

Lean4

@[to_additive (attr := simp) cmp_add_right]
theorem cmp_mul_right' {α : Type*} [Mul α] [LinearOrder α] [MulRightStrictMono α] (a b c : α) :
    cmp (a * c) (b * c) = cmp a b :=
  (strictMono_id.mul_const' c).cmp_map_eq a b

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