English
Let ps be cospherical within an affine subspace s; then all simplices with vertices in ps share the same circumcenter.
Русский
Пусть ps кососферично внутри подпространства s; тогда все симплексы с вершинами из ps имеют одинаковый circumcenter.
LaTeX
$$$\exists c \in P, \forall sx : \text{Simplex } \mathbb{R} P\, n,\; (\text{range } sx.points \subseteq ps) \Rightarrow sx.circumcenter = c$$$
Lean4
/-- Two n-simplices among cospherical points in n-space have the same
circumcenter. -/
theorem circumcenter_eq_of_cospherical {ps : Set P} {n : ℕ} [FiniteDimensional ℝ V] (hd : finrank ℝ V = n)
(hc : Cospherical ps) {sx₁ sx₂ : Simplex ℝ P n} (hsx₁ : Set.range sx₁.points ⊆ ps)
(hsx₂ : Set.range sx₂.points ⊆ ps) : sx₁.circumcenter = sx₂.circumcenter :=
by
rcases exists_circumcenter_eq_of_cospherical hd hc with ⟨r, hr⟩
rw [hr sx₁ hsx₁, hr sx₂ hsx₂]
