English
If an affine combination of affinely independent points lies in the affine span of a subset, then all weights outside that subset are zero.
Русский
Если аффинная комбинация аффинно независимых точек лежит в аффинном охвате некоторого подмножества, то все веса вне этого подмножества равны нулю.
LaTeX
$$$\\forall \\{p: ι\\to P\\},\\ ha: \\operatorname{AffineIndependent} k p\\;\\to\\forall {\\,fs: \\mathrm{Finset}\\ ι} {w: ι\\to k},\\; (\\sum_{i\\in fs} w_i = 1) \\to \\forall {s: \\mathrm{Set}\\ ι},\\; (fs.affineCombination k p w) \\in \\operatorname{affineSpan} k (p'' s) \\to \\forall i\\in fs,\\ i\\notin s \\Rightarrow w_i = 0$$$
Lean4
/-- If an affine combination of affinely independent points lies in the affine span of a subset
of those points, all weights outside that subset are zero. -/
theorem eq_zero_of_affineCombination_mem_affineSpan {p : ι → P} (ha : AffineIndependent k p) {fs : Finset ι} {w : ι → k}
(hw : ∑ i ∈ fs, w i = 1) {s : Set ι} (hm : fs.affineCombination k p w ∈ affineSpan k (p '' s)) {i : ι}
(hifs : i ∈ fs) (his : i ∉ s) : w i = 0 :=
by
obtain ⟨fs', w', hfs's, hw', he⟩ := eq_affineCombination_of_mem_affineSpan_image hm
have hi' : (fs : Set ι).indicator w i = 0 :=
by
rw [ha.indicator_eq_of_affineCombination_eq fs fs' w w' hw hw' he]
exact Set.indicator_of_notMem (Set.notMem_subset hfs's his) w'
rw [Set.indicator_apply_eq_zero] at hi'
exact hi' (Finset.mem_coe.2 hifs)
