sum_reflectionCircumcenterWeightsWithCircumcenter

English

For distinct edge vertices i1 ≠ i2, the sum of reflectionCircumcenterWeightsWithCircumcenter i1 i2 i over i equals 1.

Русский

Для различных вершин ребра i1 ≠ i2 сумма reflectionCircumcenterWeightsWithCircumcenter i1 i2 i по i равна 1.

LaTeX

$$$\sum_i reflectionCircumcenterWeightsWithCircumcenter i1 i2 i = 1 \quad (i_1 \neq i_2)$$$

Lean4

/-- `reflectionCircumcenterWeightsWithCircumcenter` sums to 1. -/
@[simp]
theorem sum_reflectionCircumcenterWeightsWithCircumcenter {n : ℕ} {i₁ i₂ : Fin (n + 1)} (h : i₁ ≠ i₂) :
    ∑ i, reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ i = 1 :=
  by
  simp_rw [sum_pointsWithCircumcenter, reflectionCircumcenterWeightsWithCircumcenter, sum_ite, sum_const, filter_or,
    filter_eq']
  rw [card_union_of_disjoint]
  · norm_num
  · simpa only [if_true, mem_univ, disjoint_singleton] using h

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