mul_le_of_one_le_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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