English
The affine combination of the points p_i with weights affineCombinationLineMapWeights equals the line map between p_i and p_j: s.affineCombination k p (affineCombinationLineMapWeights i j c) = AffineMap.lineMap (p_i) (p_j) c.
Русский
Афинное сочетание точек p_i с весами affineCombinationLineMapWeights равняется линейному отображению между p_i и p_j: ... = AffineMap.lineMap(p_i,p_j) c.
LaTeX
$$$s\affineCombination k p (affineCombinationLineMapWeights i j c) = AffineMap.lineMap (p i) (p j) c$$$
Lean4
/-- An affine combination with `affineCombinationLineMapWeights` gives the result of
`line_map`. -/
@[simp]
theorem affineCombination_affineCombinationLineMapWeights [DecidableEq ι] (p : ι → P) {i j : ι} (hi : i ∈ s)
(hj : j ∈ s) (c : k) :
s.affineCombination k p (affineCombinationLineMapWeights i j c) = AffineMap.lineMap (p i) (p j) c := by
rw [affineCombinationLineMapWeights, ← weightedVSub_vadd_affineCombination, weightedVSub_const_smul,
s.affineCombination_affineCombinationSingleWeights k p hi, s.weightedVSub_weightedVSubVSubWeights k p hj hi,
AffineMap.lineMap_apply]
