centroid_eq_affineCombination_fintype

English

If ι is finite, the centroid equals the affine combination of p over univ with weights given by centroidWeightsIndicator.

Русский

Если ι конечен, центроид равен аффинному сочетанию точек p над univ с весами centroidWeightsIndicator.

LaTeX

$$$[Fintype\\ ι] \\; \\mathrm{centroid}(k,s,p) = univ.affineCombination(k,p,s.centroidWeightsIndicator(k))$$$

Lean4

/-- The centroid as an affine combination over a `Fintype`. -/
theorem centroid_eq_affineCombination_fintype [Fintype ι] (p : ι → P) :
    s.centroid k p = univ.affineCombination k p (s.centroidWeightsIndicator k) :=
  affineCombination_indicator_subset _ _ (subset_univ _)

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