eq_touchpoint_of_isTangentAt_exsphere

English

If a point p is tangent to the exsphere at the opposite face, then p is precisely the touchpoint on i.

Русский

Если точка p касается экссферы в точке касания по i, то p совпадает с точкой касания по i.

LaTeX

$$$ (s.exsphere(\text{signs})).IsTangentAt p (\operatorname{affineSpan}_{\mathbb{R}}(\mathrm{range}(s.faceOpposite(i).points))) \Rightarrow p = s.touchpoint(\text{signs}, i) $$$

Lean4

theorem eq_touchpoint_of_isTangentAt_exsphere {signs : Finset (Fin (n + 1))} {i : Fin (n + 1)} {p : P}
    (ht : (s.exsphere signs).IsTangentAt p (affineSpan ℝ (Set.range (s.faceOpposite i).points))) :
    p = s.touchpoint signs i := by rw [ht.eq_orthogonalProjection, touchpoint, orthogonalProjectionSpan, excenter]

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