English
An affine combination, taken over the image of an embedding, equals an affine combination with the same points and weights but pulled back along the embedding.
Русский
Аффинная комбинация по образу вложенного отображения равна аффинной комбинации по тем же точкам и весам, подтянутой обратно вдоль вложения.
LaTeX
$$$ (s_2.map e).affineCombination\; k\; p\; w = s_2.affineCombination\; k\; (p \circ e) \; (w \circ e) $$$
Lean4
/-- An affine combination, over the image of an embedding, equals an
affine combination with the same points and weights over the original
`Finset`. -/
theorem affineCombination_map (e : ι₂ ↪ ι) (w : ι → k) (p : ι → P) :
(s₂.map e).affineCombination k p w = s₂.affineCombination k (p ∘ e) (w ∘ e) := by
simp_rw [affineCombination_apply, weightedVSubOfPoint_map]
