smul_add_smul_le_smul_add_smul — Mathlib

English

Let a1 ≤ a2 and b1 ≤ b2 in an ordered module with scalar multiplication, then a1·b2 + a2·b1 ≤ a1·b1 + a2·b2.

Русский

Пусть на модуле упорядочено скалярное действие и a1 ≤ a2, b1 ≤ b2. Тогда 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
  obtain ⟨a, ha₀, rfl⟩ := exists_nonneg_add_of_le ha
  rw [add_smul, add_smul, add_left_comm]
  gcongr
  assumption

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