affineCombination_affineCombinationSingleWeights

English

For any i in s, taking the affine combination with weights concentrated at i, s.affineCombination k p (affineCombinationSingleWeights k i) yields p_i.

Русский

Для любого i из s применение аффинного сочетания с весами, сосредоточенными в i, даёт p_i.

LaTeX

$$$s\.affineCombination k p (affineCombinationSingleWeights k i) = p_i$$$

Lean4

/-- An affine combination with `affineCombinationSingleWeights` gives the specified point. -/
@[simp]
theorem affineCombination_affineCombinationSingleWeights [DecidableEq ι] (p : ι → P) {i : ι} (hi : i ∈ s) :
    s.affineCombination k p (affineCombinationSingleWeights k i) = p i :=
  by
  refine s.affineCombination_of_eq_one_of_eq_zero _ _ hi (by simp) ?_
  rintro j - hj
  simp [hj]

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