English
The sign of the touchpoint weight matches the sign of the excenter weight for the corresponding vertex.
Русский
Если эксцентр существует, знак касательной точки согласуется с знаком эксцентра под линейными отображениями.
LaTeX
$$$ \operatorname{sign}( s.touchpointWeights(\text{signs}, i, j) ) = \operatorname{sign}( s.excenterWeights(\text{signs}, j) ) $$$
Lean4
theorem sign_touchpointWeights {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) {i j : Fin (n + 1)}
(hne : i ≠ j) : SignType.sign (s.touchpointWeights signs i j) = SignType.sign (s.excenterWeights signs j) :=
by
have hs := h.sign_signedInfDist_touchpoint hne
rw [← s.affineCombination_touchpointWeights signs i, h.sign_signedInfDist_excenter,
s.signedInfDist_affineCombination j (by simp)] at hs
rw [← hs, sign_mul]
convert (mul_one _).symm
rw [sign_eq_one_iff, ← dist_eq_norm_vsub]
exact s.height_pos _
