English
For a finite type ι, any p1 in the affine span of Set.range p can be expressed as a univ-affine combination with some weights summing to 1.
Русский
Для конечного типа ι каждую точку p1 в афинном span множества Set.range p можно выразить как афинное сочетание над всеми индексами с суммой весов равной 1.
LaTeX
$$$p_1 \in \affineSpan_k(\operatorname{Set.range} p) \,\Rightarrow\, \exists w:\, ι \to k, \sum_i w_i = 1 \land p_1 = \Finset.univ.affineCombination k p w$$$
Lean4
theorem eq_affineCombination_of_mem_affineSpan_of_fintype [Fintype ι] {p1 : P} {p : ι → P}
(h : p1 ∈ affineSpan k (Set.range p)) : ∃ w : ι → k, ∑ i, w i = 1 ∧ p1 = Finset.univ.affineCombination k p w := by
classical
obtain ⟨s, w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan h
refine ⟨(s : Set ι).indicator w, ?_, Finset.affineCombination_indicator_subset w p s.subset_univ⟩
simp only [Finset.mem_coe, Set.indicator_apply, ← hw]
rw [Fintype.sum_extend_by_zero s w]
