English
An illustrative instance showing the normalization of barycentric coordinates on the affine span.
Русский
Иллюстративный пример нормализации барицентрических координат на аффинном охвате.
LaTeX
$$$\sum_i b.coord i q = 1$ for q in affineSpan k (range b)$$
Lean4
@[simp]
theorem sum_coord_apply_eq_one [Fintype ι] (q : P) : ∑ i, b.coord i q = 1 :=
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
convert hw
exact b.coord_apply_combination_of_mem (Finset.mem_univ _) hw