toMulPosMono — Mathlib

English

In an ordered ring, multiplication by a nonnegative element is monotone on the right: if a ≤ b and c ≥ 0, then a c ≤ b c.

Русский

В упорядоченном кольце умножение на неотрицательное число не уменьшает порядок: если a ≤ b и c ≥ 0, то ac ≤ bc.

LaTeX

$$$ (a \\le b) \\land (c \\ge 0) \\Rightarrow (a c \\le b c). $$$

Lean4

instance (priority := 200) toMulPosMono : MulPosMono R where
  elim x _ _ h := IsOrderedRing.mul_le_mul_of_nonneg_right _ _ _ h x.2

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