English
An affine combination over the difference of two Finsets equals the difference of affine combinations with appropriately negated weights.
Русский
Аффинная комбинация над разностью Finset равна разности аффинных комбинаций с соответствующим отрицанием весов.
LaTeX
$$$$ (s \ s_2).affineCombination k p w -ᵥ s_2.affineCombination k p (-w) = s.weightedVSub p w. $$$$
Lean4
/-- Suppose an indexed family of points is given, along with a subset
of the index type. A point can be expressed as an
`affineCombination` using a `Finset` lying within that subset and
with sum of weights 1 if and only if it can be expressed an
`affineCombination` with sum of weights 1 for the corresponding
indexed family whose index type is the subtype corresponding to that
subset. -/
theorem eq_affineCombination_subset_iff_eq_affineCombination_subtype {p0 : P} {s : Set ι} {p : ι → P} :
(∃ fs : Finset ι, ↑fs ⊆ s ∧ ∃ w : ι → k, ∑ i ∈ fs, w i = 1 ∧ p0 = fs.affineCombination k p w) ↔
∃ (fs : Finset s) (w : s → k), ∑ i ∈ fs, w i = 1 ∧ p0 = fs.affineCombination k (fun i : s => p i) w :=
by
simp_rw [affineCombination_apply, eq_vadd_iff_vsub_eq]
exact eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype
