combo_eq_smul_sub_add — Mathlib

English

For a,b ∈ R with a + b = 1 and x,y ∈ M, a·x + b·y = b·(y − x) + x.

Русский

Для a,b ∈ R с a + b = 1 и x,y ∈ M верно a·x + b·y = b·(y − x) + x.

LaTeX

$$$\\forall x,y \\in M\\, \\forall a,b \\in R\\ (a+b=1)\\Rightarrow a\\cdot x + b\\cdot y = b\\cdot(y - x) + x$$$

Lean4

theorem combo_eq_smul_sub_add [Module R M] {x y : M} {a b : R} (h : a + b = 1) : a • x + b • y = b • (y - x) + x :=
  calc
    a • x + b • y = b • y - b • x + (a • x + b • x) := by rw [sub_add_add_cancel, add_comm]
    _ = b • (y - x) + x := by rw [smul_sub, Convex.combo_self h]

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