coord_apply_combination_of_mem — Mathlib

English

If i ∉ s and weights sum to 1, the i-th coordinate is 0.

Русский

Если i не принадлежит s и веса суммируются в 1, i-я координата равна 0.

LaTeX

$$$hi : i \notin s \Rightarrow wsum = 1 \Rightarrow b.coord i (s.affineCombination k b w) = 0$$$

Lean4

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

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