sum_centroidWeightsIndicator — Mathlib

English

For a finite index type ι, the sum over all i of centroidWeightsIndicator equals the sum over i in s of centroidWeights.

Русский

Для конечного типа индексов ι сумма индикаторов весов центроида равна сумме по i∈s весов центроида.

LaTeX

$$$\\sum_i s.centroidWeightsIndicator(k,i) = \\sum_{i\\in s} s.centroidWeights(k,i)$$$

Lean4

/-- The sum of the weights for the centroid indexed by a `Fintype`. -/
theorem sum_centroidWeightsIndicator [Fintype ι] :
    ∑ i, s.centroidWeightsIndicator k i = ∑ i ∈ s, s.centroidWeights k i :=
  sum_indicator_subset _ (subset_univ _)

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