English
Let s be a finite subset of P and w a weight function on s. If i : s → P is the inclusion, then the affine combination over the attached index set with weights pulled back along i equals the affine combination over s with the same weights. In symbols, AffineCombination on s.attach using (i) and w ∘ i coincides with AffineCombination on s using id and w.
Русский
Пусть s — конечное множество точек в аффинном пространстве P, и пусть w: s → k — веса. Пусть i: s ↪ P — включение. Тогда аффинная комбинация над присоединённой системой индексов с весами, предварительно перенесёнными через i, равна обычной аффинной комбинации над s с весами w.
LaTeX
$$$$\text{affineCombination}_k\bigl(s^{\mathrm{attach}},\; (\uparrow) : s \to P,\; (w \circ \uparrow)\bigr) \\ = \\text{affineCombination}_k\bigl(s,\; \mathrm{id},\; w\bigr)$$$$
Lean4
theorem attach_affineCombination_coe (s : Finset P) (w : P → k) :
s.attach.affineCombination k ((↑) : s → P) (w ∘ (↑)) = s.affineCombination k id w := by
classical
rw [attach_affineCombination_of_injective s w ((↑) : s → P) Subtype.coe_injective, univ_eq_attach, attach_image_val]
