English
For every i, the exsphere corresponding to signs is tangent at the touchpoint with i to the affine span of the opposite face.
Русский
Для каждого i экссфера, соответствующая знакам, касается касательной точки по i в аффинном проекция пространства противоположной грани.
LaTeX
$$$ (s.exsphere(\text{signs}))\IsTangentAt (s.touchpoint(\text{signs}, i)) (\operatorname{affineSpan}_{\mathbb{R}}(\mathrm{Set.range}(s.faceOpposite(i).points))) $$$
Lean4
theorem isTangentAt_touchpoint {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) (i : Fin (n + 1)) :
(s.exsphere signs).IsTangentAt (s.touchpoint signs i) (affineSpan ℝ (Set.range (s.faceOpposite i).points)) := by
rw [touchpoint, orthogonalProjectionSpan, excenter, ←
EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt, ← orthogonalProjectionSpan, ←
excenter, ← exradius, ← touchpoint, h.dist_excenter]
