English
There exists a unique circumcenter and circumradius for any finite affinely independent family of points in a Euclidean space.
Русский
Для любого конечного афинно независимого множества точек в евклидовом пространстве существует единственный циркумцентр и циркумрадиус.
LaTeX
$$$\\forall p: ι \\to P,\\; \\text{AffineIndependent}(_{\\mathbb{R}}(p)) \\Rightarrow \\exists! cs:\\ Sphere P, cs.center \\in affineSpan ℝ (Set.range p) \\land Set.range p ⊆ cs.$$$
Lean4
/-- The property satisfied by the circumsphere. -/
theorem circumsphere_unique_dist_eq {n : ℕ} (s : Simplex ℝ P n) :
(s.circumsphere.center ∈ affineSpan ℝ (Set.range s.points) ∧ Set.range s.points ⊆ s.circumsphere) ∧
∀ cs : Sphere P, cs.center ∈ affineSpan ℝ (Set.range s.points) ∧ Set.range s.points ⊆ cs → cs = s.circumsphere :=
s.independent.existsUnique_dist_eq.choose_spec
