English
Let ps be a cospherical set of points in P, and V be finite dimensional. If hd expresses that the ambient space has dimension n (finrank V = n) and hc asserts cosphericity of ps, then there exists a real number r such that every n-simplex with vertices in ps has circumradius equal to r.
Русский
Пусть ps — множество кососферических точек в P, V конечномерного размера. Пусть hd задаёт размерность пространства n и hc задаёт кососферичность ps. Тогда существует вещественное число r, такое что любая n-мерная симплексная коллекция точек из ps имеет circumradius = r.
LaTeX
$$$\exists r \in \mathbb{R}, \forall sx : \text{Simplex } \mathbb{R} P\, n,\; \{"range"\(sx.points)\} \subseteq ps \;\Rightarrow\; sx.circumradius = r$$$
Lean4
/-- All n-simplices among cospherical points in n-space have the same
circumradius. -/
theorem exists_circumradius_eq_of_cospherical {ps : Set P} {n : ℕ} [FiniteDimensional ℝ V] (hd : finrank ℝ V = n)
(hc : Cospherical ps) : ∃ r : ℝ, ∀ sx : Simplex ℝ P n, Set.range sx.points ⊆ ps → sx.circumradius = r :=
by
haveI : Nonempty (⊤ : AffineSubspace ℝ P) := Set.univ.nonempty
rw [← finrank_top, ← direction_top ℝ V P] at hd
refine exists_circumradius_eq_of_cospherical_subset ?_ hd hc
exact Set.subset_univ _
