English
Let b be an affine basis for an affine space P over k. For every point q ∈ P, the barycentric (affine) combination of the basis points b_i with weights given by the coordinates coord_i(q) equals q; i.e., q is the affine combination of the basis points with weights given by its coordinates.
Русский
Пусть b — аффинная база для аффинного пространства P над полем k. Для любой точки q ∈ P весами в разложении по базе являются координаты coord_i(q); тогда q является аффинной комбинацией точек базы b_i с весами coord_i(q).
LaTeX
$$$\\text{Finset.univ.affineCombination } k\\; b\\; (\\lambda i. b.coord\\, i\\; q) = q$$$
Lean4
@[simp]
theorem affineCombination_coord_eq_self [Fintype ι] (q : P) :
(Finset.univ.affineCombination k b fun i => b.coord i q) = q :=
by
have hq : q ∈ affineSpan k (range b) := by
rw [b.tot]
exact AffineSubspace.mem_top k V q
obtain ⟨w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hq
congr
ext i
exact b.coord_apply_combination_of_mem (Finset.mem_univ i) hw
