mul_le_mul_of_nonpos_of_nonneg' — Mathlib

English

If c ≤ a, d ≤ b with nonpos constraints, then a*b ≤ c*d.

Русский

Если выполняются условия неотрицательности и неположительности слева и справа, то неравенство сохраняется.

LaTeX

$$$ c \le a \land d \le b \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] [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

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