English
All n-simplices among cospherical points in full space have the same circumcenter; there exists c with this property, independent of the simplex chosen.
Русский
Во всей плоскости все n-мерные симплексы из кососферических точек имеют один и тот же circumcenter; существует центр, удовлетворяющий этому свойству.
LaTeX
$$$\exists c \in P, \forall sx : \text{Simplex } \mathbb{R} P\, n,\; \text{Set.range } sx.points \subseteq ps \Rightarrow sx.circumcenter = c$$$
Lean4
/-- All n-simplices among cospherical points in n-space have the same
circumcenter. -/
theorem exists_circumcenter_eq_of_cospherical {ps : Set P} {n : ℕ} [FiniteDimensional ℝ V] (hd : finrank ℝ V = n)
(hc : Cospherical ps) : ∃ c : P, ∀ sx : Simplex ℝ P n, Set.range sx.points ⊆ ps → sx.circumcenter = c :=
by
haveI : Nonempty (⊤ : AffineSubspace ℝ P) := Set.univ.nonempty
rw [← finrank_top, ← direction_top ℝ V P] at hd
refine exists_circumcenter_eq_of_cospherical_subset ?_ hd hc
exact Set.subset_univ _
