sum_excenterWeights — Mathlib

English

The sum of excenter weights across all vertex indices equals 1 when the excenter exists, otherwise 0.

Русский

Сумма весов эксцентра по всем вершинам равна 1, если эксцентр существует, иначе 0.

LaTeX

$$$\sum_i s.excenterWeights(signs) i = \begin{cases} 1, & s.ExcenterExists(signs) \\ 0, & \text{otherwise} \end{cases}$$$

Lean4

theorem sum_excenterWeights (signs : Finset (Fin (n + 1))) [Decidable (s.ExcenterExists signs)] :
    ∑ i, s.excenterWeights signs i = if s.ExcenterExists signs then 1 else 0 :=
  by
  simp_rw [ExcenterExists, excenterWeights]
  split_ifs with h
  · simp [← Finset.mul_sum, h]
  · simp only [ne_eq, not_not] at h
    simp [h]

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