signedInfDist_excenter_eq_mul_sum_inv

English

For any signs, the signed distance from the excenter to the plane of each face satisfies the same reciprocal relation as above.

Русский

Для любых знаков расстояние между экцентром и плоскостью каждой грани удовлетворяет той же обратной зависимости, как и ранее.

LaTeX

$$s.signedInfDist i (s.excenter signs) = (if i ∈ signs then -1 else 1) * (\sum j, s.excenterWeightsUnnorm signs j)^{-1}$$

Lean4

theorem signedInfDist_excenter_eq_mul_sum_inv {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs)
    (i : Fin (n + 1)) :
    s.signedInfDist i (s.excenter signs) = (if i ∈ signs then -1 else 1) * (∑ j, s.excenterWeightsUnnorm signs j)⁻¹ :=
  by
  simp_rw [excenter_eq_affineCombination, signedInfDist_affineCombination _ _ h.sum_excenterWeights_eq_one,
    excenterWeights, Pi.smul_apply, ← dist_eq_norm_vsub, excenterWeightsUnnorm]
  rw [← altitudeFoot, ← height]
  simp [(s.height_pos i).ne']

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