mul_add_mul_le_mul_add_mul' — Mathlib

English

If b ≤ a and d ≤ c, then a d + b c ≤ a c + b d.

Русский

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

LaTeX

$$$b \le a \wedge d \le c \Rightarrow a d + b c \le a c + b d$$$

Lean4

/-- Binary **rearrangement inequality**. -/
theorem mul_add_mul_le_mul_add_mul' [ExistsAddOfLE R] [MulPosMono R] [AddLeftMono R] [AddLeftReflectLE R] (hba : b ≤ a)
    (hdc : d ≤ c) : a * d + b * c ≤ a * c + b * d := by rw [add_comm (a * d), add_comm (a * c)];
  exact mul_add_mul_le_mul_add_mul hba hdc

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