affineCombination_indicator_subset

English

If s1 ⊆ s2, then the affine combination over s1 with weights w equals the affine combination over s2 with weights indicator of s1.

Русский

Если s1 ⊆ s2, то аффинная комбинация по s1 с весами w равна аффинной комбинации по s2 с весами indicator(s1) w.

LaTeX

$$$ s_1.affineCombination\; k\; p\; w = s_2.affineCombination\; k\; p\; (\mathrm{Set.indicator}(\uparrow s_1)\, w)$$$

Lean4

/-- An affine combination is unaffected by changing the weights to the
corresponding indicator function and adding points to the set. -/
theorem affineCombination_indicator_subset (w : ι → k) (p : ι → P) {s₁ s₂ : Finset ι} (h : s₁ ⊆ s₂) :
    s₁.affineCombination k p w = s₂.affineCombination k p (Set.indicator (↑s₁) w) := by
  rw [affineCombination_apply, affineCombination_apply, weightedVSubOfPoint_indicator_subset _ _ _ h]

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