mul_le_mul_of_nonneg_of_nonpos — Mathlib

English

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

Русский

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

LaTeX

$$$ c \le a \land b \le d \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] [MulPosMono R] [PosMulMono R] [AddRightMono R]
    [AddRightReflectLE R] (hca : c ≤ a) (hbd : b ≤ d) (hc : 0 ≤ c) (hb : b ≤ 0) : a * b ≤ c * d :=
  (mul_le_mul_of_nonpos_right hca hb).trans <| mul_le_mul_of_nonneg_left hbd hc

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