sum_excenterWeights_eq_one_iff — Mathlib

English

Let s be an affine simplex in a real Euclidean space. For any collection of vertex-indices signs, the sum of the excenter weights equals 1 precisely when an excenter exists corresponding to those signs.

Русский

Пусть s — аффинная симплексная фигура в евклидовом пространстве над реалами. Для любой конечной подмножества индексов вершин signs сумма весов эксцентра равна 1 тогда и только тогда существует эксцентр, соответствующий этим знакам.

LaTeX

$$$\displaystyle \sum_i s.excenterWeights signs\, i = 1 \quad\text{iff}\quad s.ExcenterExists signs$$

Lean4

@[simp]
theorem sum_excenterWeights_eq_one_iff {signs : Finset (Fin (n + 1))} :
    ∑ i, s.excenterWeights signs i = 1 ↔ s.ExcenterExists signs := by classical simp [sum_excenterWeights]

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