toMulPosMono — Mathlib

English

In a linear ordered commutative group with zero, left multiplication by any element preserves order. Equivalently, for all a, b, c in the group, if b ≤ c then a b ≤ a c.

Русский

В линейно упорядоченной коммутативной группе с нулём левое умножение на любой элемент сохраняет порядок: для всех a, b, c в группе, если b ≤ c, то a b ≤ a c.

LaTeX

$$$\\\\forall a,b,c \\\\in \\\\alpha,\\\\ b \\\\le c \\\\Rightarrow a b \\\\le a c$$$

Lean4

instance (priority := 100) toMulPosMono : MulPosMono α where
  elim _a _b _c
    hbc :=
    mul_le_mul_right' hbc
      _
        -- See note [lower instance priority]

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