English
Affine combinations commute with embeddings: the affine combination over the image of an embedding e of a finite set s₂ equals the affine combination over s₂ with the composed point function and weight function, i.e. (s₂.map e).affineCombination k p w = s₂.affineCombination k (p ∘ e) (w ∘ e).
Русский
Аффинные комбинации commute с вложениями: аффинная комбинация над образа вложения e равна аффинной комбинации над исходным множеством с композициями p и w.
LaTeX
$$$$ (s_2\text{.map } e).\text{affineCombination}_k(p,w) = s_2.\text{affineCombination}_k(p\circ e, w\circ e). $$$$
Lean4
/-- An `affineCombination` equals a point if that point is in the set
and has weight 1 and the other points in the set have weight 0. -/
-- Cannot be @[simp] because `i` cannot be inferred by `simp`.
theorem affineCombination_of_eq_one_of_eq_zero (w : ι → k) (p : ι → P) {i : ι} (his : i ∈ s) (hwi : w i = 1)
(hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0) : s.affineCombination k p w = p i :=
by
have h1 : ∑ i ∈ s, w i = 1 := hwi ▸ sum_eq_single i hw0 fun h => False.elim (h his)
rw [s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p h1 (p i), weightedVSubOfPoint_apply]
convert zero_vadd V (p i)
refine sum_eq_zero ?_
intro i2 hi2
by_cases h : i2 = i
· simp [h]
· simp [hw0 i2 hi2 h]
