mul_add_mul_le_mul_add_mul — Mathlib

English

Let a ≤ b and c ≤ d. Then a d + b c ≤ a c + b d.

Русский

Пусть a ≤ b и c ≤ d. Тогда a d + b c ≤ a c + b d.

LaTeX

$$$a \le b \wedge c \le d \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] (hab : a ≤ b)
    (hcd : c ≤ d) : a * d + b * c ≤ a * c + b * d :=
  by
  obtain ⟨d, hd, rfl⟩ := exists_nonneg_add_of_le hcd
  rw [mul_add, add_right_comm, mul_add, ← add_assoc]
  exact add_le_add_left (mul_le_mul_of_nonneg_right hab hd) _

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