English
For a simplex s, the circumsphere cs has the property that its center lies in the affine span of the vertices and the vertices are contained in cs; moreover, cs is the unique sphere with this property.
Русский
Для многогранника circumsphere обладает следующими свойствами: центр лежит во афинном охвате вершин, вершины принадлежат circumsphere, и circumsphere уникальна по этим свойствам.
LaTeX
$$$(s.circumsphere.center \\in affineSpan ℝ (Set.range s.points)) \\land (Set.range s.points \\subset s.circumsphere) \\land \\forall (cs : Sphere P), cs.center \\in affineSpan ℝ (Set.range s.points) \\land Set.range s.points \\subset cs \\rightarrow cs = s.circumsphere$$$
Lean4
/-- The circumcenter of a simplex. -/
def circumcenter {n : ℕ} (s : Simplex ℝ P n) : P :=
s.circumsphere.center
