English
Distance identities between excenter and touchpoints hold for the given signs across faces.
Русский
Расстояния между эксцентром и точками касания по заданным граням сохраняются.
LaTeX
$$dist (s.excenter signs) (s.touchpoint signs i) = s.exradius signs$$
Lean4
/-- The distance between the excenter and its projection in the plane of each face is the
exradius. -/
theorem dist_excenter {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) (i : Fin (n + 1)) :
dist (s.excenter signs) (s.touchpoint signs i) = s.exradius signs :=
by
rw [touchpoint, ← abs_signedInfDist_eq_dist_of_mem_affineSpan_range i h.excenter_mem_affineSpan_range,
h.signedInfDist_excenter, abs_mul, abs_mul, abs_of_nonneg (s.exradius_nonneg signs)]
simp only [abs_ite, abs_neg, abs_one, ite_self, one_mul]
rcases lt_trichotomy 0 (∑ i, s.excenterWeightsUnnorm signs i) with h' | h' | h'
· simp [h']
· simp [h h'.symm]
· simp [h']
