toMulPosReflectLE — Mathlib

English

Left multiplication by a positive element is order-reflecting: if a b ≤ a c, then b ≤ c, provided a > 0.

Русский

Отражение порядка левым умножением на положительный элемент: если a b ≤ a c, то b ≤ c, при a > 0.

LaTeX

$$$\\\\forall a,b,c \\\\in \\\\alpha, \\\\ 0 < a \\\\Rightarrow (a b \\\\le a c \\\\Rightarrow b \\\\le c)$$$

Lean4

instance (priority := 100) toMulPosReflectLE : MulPosReflectLE α where
  elim a b c
    hbc := by
    simpa [a.2.ne'] using
      mul_le_mul_right' hbc
        a⁻¹
          -- See note [lower instance priority]

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