sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one

English

If s.card = n+1, then ∑ i, s.centroidWeightsIndicator k i = 1.

Русский

Если card(s) = n+1, то сумма индикаторов весов центроида равна 1.

LaTeX

$$$[CharZero\\ k] [Fintype\\ ι] {n : \\mathbb{N}} (h : s.card = n+1) : \\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 `n + 1`. -/
theorem sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one [CharZero k] [Fintype ι] {n : ℕ} (h : #s = n + 1) :
    ∑ i, s.centroidWeightsIndicator k i = 1 :=
  by
  rw [sum_centroidWeightsIndicator]
  exact s.sum_centroidWeights_eq_one_of_card_eq_add_one k h

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