sign_touchpointWeights_singleton_neg

English

For i ≠ j, the weight s.touchpointWeights { i } j i has negative sign:

Русский

Для i ≠ j вес s.touchpointWeights { i } j i имеет отрицательный знак.

LaTeX

$$$\operatorname{sign}\bigl(s.touchpointWeights\{i\} j i\bigr) = -1\quad (i \neq j)$$$

Lean4

theorem sign_touchpointWeights_singleton_neg [Nat.AtLeastTwo n] {i j : Fin (n + 1)} (hne : i ≠ j) :
    SignType.sign (s.touchpointWeights { i } j i) = -1 := by
  rw [(s.excenterExists_singleton i).sign_touchpointWeights hne.symm, s.sign_excenterWeights_singleton_neg]

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