touchpoint — Mathlib

English

The touchpoint is the orthogonal projection of the excenter onto the faceOpposite i.

Русский

Touchpoint есть ортогональная проекция эксцентра на грань противоположную вершине i.

LaTeX

$$s.touchpoint(signs,i) = (s.faceOpposite i).orthogonalProjectionSpan (s.excenter signs)$$

Lean4

/-- A touchpoint is where an exsphere of a simplex is tangent to one of the faces. -/
def touchpoint (signs : Finset (Fin (n + 1))) (i : Fin (n + 1)) : P :=
  (s.faceOpposite i).orthogonalProjectionSpan (s.excenter signs)

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