affineCombination_filter_of_ne — Mathlib

English

Affine combinations over subtype s of indices equal the affine combinations over the original indices with the same weights, interpreted through the subtype.

Русский

Аффинные комбинации по подтипу индексов равны аффинным комбинациям по исходным индексам с теми же весами, через подтип.

LaTeX

$$$$ s.\affineCombination_k(p, w) = s'.\affineCombination_k(p|_s, w|_s). $$$$

Lean4

/-- An affine combination over `{x ∈ s | pred x}` equals one over `s` if all the weights at indices
in `s` not satisfying `pred` are zero. -/
theorem affineCombination_filter_of_ne (w : ι → k) (p : ι → P) {pred : ι → Prop} [DecidablePred pred]
    (h : ∀ i ∈ s, w i ≠ 0 → pred i) : {x ∈ s | pred x}.affineCombination k p w = s.affineCombination k p w := by
  rw [affineCombination_apply, affineCombination_apply, s.weightedVSubOfPoint_filter_of_ne _ _ _ h]

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