mul_le_mul_of_nonpos_of_nonneg — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem mul_le_mul_of_nonpos_of_nonneg [ExistsAddOfLE R] [MulPosMono R] [PosMulMono R] [AddRightMono R]
    [AddRightReflectLE R] (hac : a ≤ c) (hdb : d ≤ b) (hc : c ≤ 0) (hb : 0 ≤ b) : a * b ≤ c * d :=
  (mul_le_mul_of_nonneg_right hac hb).trans <| mul_le_mul_of_nonpos_left hdb hc

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