mul_le_mul_of_nonpos_left — Mathlib

English

If c ≤ a and d ≤ b with c ≥ 0 and b ≤ 0, then a*b ≤ c*d.

Русский

Если c ≤ a и d ≤ b при условии c ≥ 0 и b ≤ 0, то a*b ≤ c*d.

LaTeX

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

Lean4

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

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