signedInfDist_excenter — Mathlib

English

The distance between the excenter and its touchpoint on a face equals the exradius.

Русский

Расстояние между эксцентром иTouchpoint на грани равно эксрадиусу.

LaTeX

$$dist (s.excenter signs) (s.touchpoint signs i) = s.exradius signs$$

Lean4

/-- The signed distance between the excenter and its projection in the plane of each face is the
exradius. -/
theorem signedInfDist_excenter {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) * SignType.sign (∑ j, s.excenterWeightsUnnorm signs j) * (s.exradius signs) :=
  by
  rw [h.signedInfDist_excenter_eq_mul_sum_inv, mul_assoc, exradius_eq_abs_inv_sum]
  congr
  rw [← mul_eq_one_iff_inv_eq₀ h, ← mul_assoc, self_mul_sign, ← abs_mul, mul_inv_cancel₀ h, abs_one]

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