sum_centroidWeightsWithCircumcenter

English

If the finite set fs is nonempty, the sum of centroidWeightsWithCircumcenter fs over all i equals 1.

Русский

Если fs непусто, сумма centroidWeightsWithCircumcenter fs по всем i равна 1.

LaTeX

$$$fs.Nonempty \Rightarrow \sum_i centroidWeightsWithCircumcenter fs i = 1$$$

Lean4

/-- `centroidWeightsWithCircumcenter` sums to 1, if the `Finset` is nonempty. -/
@[simp]
theorem sum_centroidWeightsWithCircumcenter {n : ℕ} {fs : Finset (Fin (n + 1))} (h : fs.Nonempty) :
    ∑ i, centroidWeightsWithCircumcenter fs i = 1 :=
  by
  simp_rw [sum_pointsWithCircumcenter, centroidWeightsWithCircumcenter, add_zero, ←
    fs.sum_centroidWeights_eq_one_of_nonempty ℝ h, ← sum_indicator_subset _ fs.subset_univ]
  rcongr

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