sign_excenterWeights_empty — Mathlib

English

For every vertex index i, the sign of s.excenterWeights ∅ i is +1.

Русский

Для каждого индекса вершины i знак s.excenterWeights ∅ i равен +1.

LaTeX

$$$\operatorname{sign}\bigl(s.excenterWeights \emptyset i\bigr) = 1$$$

Lean4

@[simp]
theorem sign_excenterWeights_empty (i : Fin (n + 1)) : SignType.sign (s.excenterWeights ∅ i) = 1 :=
  by
  simp only [excenterWeights, excenterWeightsUnnorm_empty_apply, Pi.smul_apply, smul_eq_mul]
  rw [sign_eq_one_iff]
  positivity

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