toPosMulMono — Mathlib

English

Left multiplication by any element is order-preserving: for all a, b, c ∈ α, if b ≤ c then b a ≤ c a.

Русский

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

LaTeX

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

Lean4

instance (priority := 100) toPosMulMono : PosMulMono α where
  elim _a _b _c
    hbc :=
    mul_le_mul_left' hbc
      _
        -- See note [lower instance priority]

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