English
If ps is a cospherical set contained in an affine subspace s, then all n-simplices with vertices in ps have the same circumcenter.
Русский
Еслиps кососферично и содержится в аффинном подпространстве s, то все n-мерные симплексы с вершинами в ps имеют один и тот же circumcenter.
LaTeX
$$$\forall sx_1, sx_2 : \text{Simplex } \mathbb{R} P\, n,\; (\text{range } sx_1.points \subseteq ps) \land (\text{range } sx_2.points \subseteq ps) \Rightarrow sx_1.circumcenter = sx_2.circumcenter$$$
Lean4
/-- Two n-simplices among cospherical points in an n-dimensional
subspace have the same circumcenter. -/
theorem circumcenter_eq_of_cospherical_subset {s : AffineSubspace ℝ P} {ps : Set P} (h : ps ⊆ s) [Nonempty s] {n : ℕ}
[FiniteDimensional ℝ s.direction] (hd : finrank ℝ s.direction = 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_subset h hd hc with ⟨r, hr⟩
rw [hr sx₁ hsx₁, hr sx₂ hsx₂]
