English
The sum over all circumcenter-related indices equals the sum over vertex indices plus the circumcenter index contribution.
Русский
Сумма по всем индексам circumcenter равна сумме по вершинам плюс вклад circumcenter индекса.
LaTeX
$$$\sum_{i\in(PointsWithCircumcenterIndex\,n)} f(i) = \sum_{i=0}^{n} f(pointIndex(i)) + f(circumcenterIndex)$$$
Lean4
/-- The sum of a function over `PointsWithCircumcenterIndex`. -/
theorem sum_pointsWithCircumcenter {α : Type*} [AddCommMonoid α] {n : ℕ} (f : PointsWithCircumcenterIndex n → α) :
∑ i, f i = (∑ i : Fin (n + 1), f (pointIndex i)) + f circumcenterIndex := by
classical
have h : univ = insert circumcenterIndex (univ.map (pointIndexEmbedding n)) :=
by
ext x
refine ⟨fun h => ?_, fun _ => mem_univ _⟩
obtain i | - := x
· exact mem_insert_of_mem (mem_map_of_mem _ (mem_univ i))
· exact mem_insert_self _ _
change _ = (∑ i, f (pointIndexEmbedding n i)) + _
rw [add_comm, h, ← sum_map, sum_insert]
simp_rw [Finset.mem_map, not_exists]
rintro x ⟨_, h⟩
injection h
