mul_le_mul_of_nonneg_of_nonpos' — Mathlib

English

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

Русский

Если выполняются условия c ≤ a, d ≤ b, 0 ≤ c и 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_nonneg_of_nonpos' [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R]
    [AddRightReflectLE R] (hca : c ≤ a) (hbd : b ≤ d) (ha : 0 ≤ a) (hd : d ≤ 0) : a * b ≤ c * d :=
  (mul_le_mul_of_nonneg_left hbd ha).trans <| mul_le_mul_of_nonpos_right hca hd

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