excenter — Mathlib

English

The excenter is defined as the center of the corresponding exsphere.

Русский

Эксцентр определяется как центр соответствующей экс сферы.

LaTeX

$$excenter(signs) = (s.exsphere signs).center$$

Lean4

/-- The excenter with signs determined by the given set of indices (for the empty set, this is
the incenter; for a singleton set, this is the excenter opposite a vertex).  This is only
meaningful if `s.ExcenterExists signs`; otherwise, it is some arbitrary point. -/
def excenter (signs : Finset (Fin (n + 1))) : P :=
  (s.exsphere signs).center

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