sum_coord_apply_eq_one — Mathlib

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

Похожие утверждения