sign_signedInfDist_touchpoint_empty

English

The touchpoint weights sum to one and respect symmetry with opposite faces.

Русский

Сумма весов касательных точек по всем i равна единице и весовые коэффициенты симметричны по отношению к противоположным граням.

LaTeX

$$$ \sum_i s.touchpointWeights(\text{signs}, i, j) = 1 \quad \text{for all } j $$$

Lean4

theorem sign_signedInfDist_touchpoint_empty {i j : Fin (n + 1)} (hne : i ≠ j) :
    SignType.sign (s.signedInfDist j (s.touchpoint ∅ i)) = SignType.sign (s.signedInfDist j s.incenter) :=
  s.excenterExists_empty.sign_signedInfDist_touchpoint hne

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