smul_add_smul_lt_smul_add_smul — Mathlib

English

If a1 < a2 and b1 < b2 in an ordered module, 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} < a_{1} \cdot b_{1} + a_{2} \cdot b_{2}$$$

Lean4

/-- Binary strict **rearrangement inequality**. -/
theorem smul_add_smul_lt_smul_add_smul (ha : a₁ < a₂) (hb : b₁ < b₂) : a₁ • b₂ + a₂ • b₁ < a₁ • b₁ + a₂ • b₂ :=
  by
  obtain ⟨a, ha₀, rfl⟩ := lt_iff_exists_pos_add.1 ha
  rw [add_smul, add_smul, add_left_comm]
  gcongr
  assumption

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