sum_excenterWeightsUnnorm_empty_pos

English

The sum of the unnormalized excenter weights over all vertices with the empty sign set is strictly positive.

Русский

Сумма не нормированных весов эксцентра по всем вершинам при пустом наборе сигналов строго положительна.

LaTeX

$$$0 < \sum_i s.excenterWeightsUnnorm \emptyset i$$

Lean4

theorem sum_excenterWeightsUnnorm_empty_pos : 0 < ∑ i, s.excenterWeightsUnnorm ∅ i :=
  by
  simp_rw [excenterWeightsUnnorm_empty_apply]
  positivity

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