le_mul_of_le_one_left — 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_left` for `b` non-positive instead of non-negative. -/
theorem le_mul_of_le_one_left [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hb : b ≤ 0)
    (h : a ≤ 1) : b ≤ a * b := by simpa only [one_mul] using mul_le_mul_of_nonpos_right h hb

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