sum_mongePointVSubFaceCentroidWeightsWithCircumcenter

English

For any n, the sum over all indices i of mongePointWeightsWithCircumcenter n i equals 1.

Русский

Для любого n сумма весов mongePointWeightsWithCircumcenter n i по всем i равна 1.

LaTeX

$$$$ \sum_i mongePointWeightsWithCircumcenter n i = 1. $$$$

Lean4

/-- `mongePointVSubFaceCentroidWeightsWithCircumcenter` sums to 0. -/
@[simp]
theorem sum_mongePointVSubFaceCentroidWeightsWithCircumcenter {n : ℕ} {i₁ i₂ : Fin (n + 3)} (h : i₁ ≠ i₂) :
    ∑ i, mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ i = 0 :=
  by
  rw [mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub h]
  simp_rw [Pi.sub_apply, sum_sub_distrib, sum_mongePointWeightsWithCircumcenter]
  rw [sum_centroidWeightsWithCircumcenter, sub_self]
  simp [← card_pos, card_compl, h]

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