coord_apply_combination_of_notMem

English

The sum over i of coord i evaluated at q equals 1 for any q in the affine span of the basis.

Русский

Сумма по i координат, применённых к q, равна 1 для любого q в аффинном охвате базиса.

LaTeX

$$$\sum_i b.coord i q = 1$$$

Lean4

@[simp]
theorem coord_apply_combination_of_notMem (hi : i ∉ s) {w : ι → k} (hw : s.sum w = 1) :
    b.coord i (s.affineCombination k b w) = 0 := by
  classical
    simp only [coord_apply, hi, Finset.affineCombination_eq_linear_combination, if_false, mul_boole, hw,
    Function.comp_apply, smul_eq_mul, s.sum_ite_eq, s.map_affineCombination b w hw]

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