sign_touchpointWeights_singleton_pos

English

For a nondegenerate affine simplex s and distinct indices i ≠ j, the sign of the touchpoint weight with singleton {i} and positions i,j equals +1.

Русский

Для невырожденного аффинного простого множества s и различных индексов i ≠ j знак веса касательной точки с единичным множеством {i} и позициями i,j равен +1.

LaTeX

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

Lean4

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

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