sign_signedInfDist_excenter — Mathlib

English

The sign of the signedInfDist equals the sign of the corresponding excenter weight.

Русский

Знак подписи расстояния совпадает с соглавной весовой функцией эксцентра.

LaTeX

$$SignType.sign(s.signedInfDist i (s.excenter signs)) = SignType.sign (s.excenterWeights signs i)$$

Lean4

theorem sign_signedInfDist_excenter {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) (i : Fin (n + 1)) :
    SignType.sign (s.signedInfDist i (s.excenter signs)) = SignType.sign (s.excenterWeights signs i) :=
  by
  rw [excenter_eq_affineCombination, signedInfDist_affineCombination _ _ h.sum_excenterWeights_eq_one, sign_mul]
  convert mul_one _
  rw [sign_eq_one_iff, ← dist_eq_norm_vsub]
  exact s.height_pos _

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