sum_pointWeightsWithCircumcenter — Mathlib

English

For any vertex i, the sum of pointWeightsWithCircumcenter i j over all j equals 1.

Русский

Для любого вершина i сумма весов pointWeightsWithCircumcenter i j по всем j равна 1.

LaTeX

$$$\sum_j pointWeightsWithCircumcenter(i,j) = 1$$$

Lean4

/-- `point_weights_with_circumcenter` sums to 1. -/
@[simp]
theorem sum_pointWeightsWithCircumcenter {n : ℕ} (i : Fin (n + 1)) : ∑ j, pointWeightsWithCircumcenter i j = 1 := by
  classical
  convert sum_ite_eq' univ (pointIndex i) (Function.const _ (1 : ℝ)) with j
  · cases j <;> simp [pointWeightsWithCircumcenter]
  · simp

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