English
Affine maps commute with affine combinations: applying an affine map f to the affine combination over s yields the affine combination over the image with f applied to the points.
Русский
Аффинные отображения commute с аффинными комбинациями: применение отображения f к комбинации в s даёт комбинацию над образами точек под действием f.
LaTeX
$$$$ f\bigl(s.affineCombination k p w\bigr) = s.affineCombination k (f\circ p) w $$$$
Lean4
/-- Affine maps commute with affine combinations. -/
theorem map_affineCombination {V₂ P₂ : Type*} [AddCommGroup V₂] [Module k V₂] [AffineSpace V₂ P₂] (p : ι → P)
(w : ι → k) (hw : s.sum w = 1) (f : P →ᵃ[k] P₂) : f (s.affineCombination k p w) = s.affineCombination k (f ∘ p) w :=
by
have b := Classical.choice (inferInstance : AffineSpace V P).nonempty
have b₂ := Classical.choice (inferInstance : AffineSpace V₂ P₂).nonempty
rw [s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p hw b,
s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w (f ∘ p) hw b₂, ←
s.weightedVSubOfPoint_vadd_eq_of_sum_eq_one w (f ∘ p) hw (f b) b₂]
simp only [weightedVSubOfPoint_apply, RingHom.id_apply, AffineMap.map_vadd, LinearMap.map_smulₛₗ,
AffineMap.linearMap_vsub, map_sum, Function.comp_apply]
