mul_le_mul_of_nonpos_right — Mathlib

English

If c ≤ a, d ≤ b, 0 ≤ a, d ≤ 0, then a*b ≤ c*d.

Русский

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

LaTeX

$$$ c \le a, \ b \le d, \ 0 \le a, \ d \le 0 \Rightarrow a \cdot b \le c \cdot d $$$

Lean4

theorem mul_le_mul_of_nonpos_right [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (h : b ≤ a)
    (hc : c ≤ 0) : a * c ≤ b * c := by
  obtain ⟨d, hcd⟩ := exists_add_of_le hc
  refine le_of_add_le_add_right (a := b * d + a * d) ?_
  calc
    _ = b * d := by rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
    _ ≤ a * d := (mul_le_mul_of_nonneg_right h <| hcd.trans_le <| add_le_of_nonpos_left hc)
    _ = _ := by rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]

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