English
If all points p(i) in the family are equal to a fixed point p, then the affine combination with weights w yields p, provided the sum of weights is 1.
Русский
Если все точки p(i) одинаковы и равны p, а сумма весов равна 1, то аффинная комбинация равна p.
LaTeX
$$$ s.affineCombination k p w = p \quad\text{whenever } \sum_{i \in s} w(i) = 1, \; p_i = p$$$
Lean4
/-- Applying `affineCombination` with given weights. This is for the
case where a result involving a default base point is OK (for example,
when that base point will cancel out later); a more typical use case
for `affineCombination` would involve selecting a preferred base
point with
`affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one` and
then using `weightedVSubOfPoint_apply`. -/
theorem affineCombination_apply (w : ι → k) (p : ι → P) :
(s.affineCombination k p) w =
s.weightedVSubOfPoint p (Classical.choice S.nonempty) w +ᵥ Classical.choice S.nonempty :=
rfl
