English
Alternative expression of affineCombination_map in terms of the same data arranged differently; the equality holds.
Русский
Альтернативное выражение affineCombination_map.
LaTeX
$$$$ \text{(см. предыдущую формулировку, эквивалентная форма)} $$$$
Lean4
/-- The value of `affineCombination`, where the given points take only two values. -/
theorem affineCombination_apply_eq_lineMap_sum [DecidableEq ι] (w : ι → k) (p : ι → P) (p₁ p₂ : P) (s' : Finset ι)
(h : ∑ i ∈ s, w i = 1) (hp₂ : ∀ i ∈ s ∩ s', p i = p₂) (hp₁ : ∀ i ∈ s \ s', p i = p₁) :
s.affineCombination k p w = AffineMap.lineMap p₁ p₂ (∑ i ∈ s ∩ s', w i) :=
by
rw [s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p h p₁, weightedVSubOfPoint_apply, ←
s.sum_inter_add_sum_diff s', AffineMap.lineMap_apply, vadd_right_cancel_iff, sum_smul]
convert add_zero _ with i hi
· convert Finset.sum_const_zero with i hi
simp [hp₁ i hi]
· exact (hp₂ i hi).symm
