sum_centroidWeightsIndicator_eq_one_of_card_ne_zero

English

In CharZero with a finite index set, if s ≠ ∅, then the total sum of centroidWeightsIndicator over all i equals 1.

Русский

В CharZero, если s непусто, сумма всех centroidWeightsIndicator равна 1.

LaTeX

$$$[CharZero\\ k] [Fintype\\ ι] (h: s.card \\neq 0) : \\sum_i s.centroidWeightsIndicator(k,i) = 1$$$

Lean4

/-- In the characteristic zero case, the weights in the centroid
indexed by a `Fintype` sum to 1 if the number of points is not
zero. -/
theorem sum_centroidWeightsIndicator_eq_one_of_card_ne_zero [CharZero k] [Fintype ι] (h : #s ≠ 0) :
    ∑ i, s.centroidWeightsIndicator k i = 1 :=
  by
  rw [sum_centroidWeightsIndicator]
  exact s.sum_centroidWeights_eq_one_of_card_ne_zero k h

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