English
If the family is nonempty, an affine combination with sum-1 weights lies in the affine span of the indexed family.
Русский
Если множество индексов непусто, то аффинное сочетание с суммой весов 1 принадлежит афинному запредельному пространству.
LaTeX
$$$s\text{ nonempty} \Rightarrow s.affineCombination k p w \in \affineSpan_k(\{ p_i : i \in s\})$$$
Lean4
/-- An `affineCombination` with sum of weights 1 is in the
`affineSpan` of an indexed family, if the family is nonempty. -/
theorem affineCombination_mem_affineSpan_of_nonempty [Nonempty ι] {s : Finset ι} {w : ι → k} (h : ∑ i ∈ s, w i = 1)
(p : ι → P) : s.affineCombination k p w ∈ affineSpan k (Set.range p) :=
by
rcases subsingleton_or_nontrivial k with hs | hn
· have hnv := Module.subsingleton k V
rw [AddTorsor.subsingleton_iff V P] at hnv
rw [(affineSpan_eq_top_iff_nonempty_of_subsingleton k).2 (Set.range_nonempty p)]
simp
· exact affineCombination_mem_affineSpan h p
