le_tsub_mul — Mathlib

English

In a similar setting, a·c − b·c ≤ (a − b)·c for all a,b,c.

Русский

В аналогичной обстановке a·c − b·c ≤ (a − b)·c для любых a,b,c.

LaTeX

$$$\forall a,b,c\in R\,(a \cdot c - b \cdot c \le (a - b) \cdot c)$$$

Lean4

theorem le_tsub_mul {R : Type*} [NonUnitalCommSemiring R] [Preorder R] [Sub R] [OrderedSub R] [MulLeftMono R]
    {a b c : R} : a * c - b * c ≤ (a - b) * c := by simpa only [mul_comm _ c] using le_mul_tsub

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