toPosMulReflectLE — Mathlib

English

Left multiplication by a positive element is an order-embedding: for all a > 0 and b, c ∈ α, we have a b ≤ a c implies b ≤ c (and conversely).

Русский

Левое умножение на положительный элемент является вложением порядка: для любого a > 0 и b, c ∈ α, a b ≤ a c подразумевает b ≤ c (и наоборот).

LaTeX

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

Lean4

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

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