le_mul_of_le_one_right — Mathlib

English

If b ≤ 0 and a ≤ 1, then b ≤ a*b.

Русский

Если b ≤ 0 и a ≤ 1, то b ≤ a*b.

LaTeX

$$$ b \le 0 \land a \le 1 \Rightarrow b \le a \cdot b $$$

Lean4

/-- Variant of `mul_le_of_le_one_right` for `a` non-positive instead of non-negative. -/
theorem le_mul_of_le_one_right [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (ha : a ≤ 0)
    (h : b ≤ 1) : a ≤ a * b := by simpa only [mul_one] using mul_le_mul_of_nonpos_left h ha

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