smul_add_smul_le_smul_add_smul' — Mathlib

English

If a2 ≤ a1 and b2 ≤ b1 in an ordered setting, then a1·b2 + a2·b1 ≤ a1·b1 + a2·b2.

Русский

Если a2 ≤ a1 и b2 ≤ b1 в упорядоченном контексте, то a1·b2 + a2·b1 ≤ a1·b1 + a2·b2.

LaTeX

$$$a_{1} \cdot b_{2} + a_{2} \cdot b_{1} \le a_{1} \cdot b_{1} + a_{2} \cdot b_{2}$$$

Lean4

/-- Binary **rearrangement inequality**. -/
theorem smul_add_smul_le_smul_add_smul' (ha : a₂ ≤ a₁) (hb : b₂ ≤ b₁) : a₁ • b₂ + a₂ • b₁ ≤ a₁ • b₁ + a₂ • b₂ := by
  simp_rw [add_comm (a₁ • _)]; exact smul_add_smul_le_smul_add_smul ha hb

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