mul_add_mul_lt_mul_add_mul — Mathlib

English

If 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 < b \wedge c < d \Rightarrow a d + b c < a c + b d$$$

Lean4

/-- Binary strict **rearrangement inequality**. -/
theorem mul_add_mul_lt_mul_add_mul [ExistsAddOfLE R] [MulPosStrictMono R] [AddLeftStrictMono R] (hab : a < b)
    (hcd : c < d) : a * d + b * c < a * c + b * d :=
  by
  obtain ⟨d, hd, rfl⟩ := exists_pos_add_of_lt' hcd
  rw [mul_add, add_right_comm, mul_add, ← add_assoc]
  gcongr
  exact hd

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