English
Let ps be a cospherical set of points in P and V finite dimensional with hd and hc as above. Then for any two n-simplices sx1 and sx2 whose vertex ranges lie in ps, their circumradius are equal to each other.
Русский
Пусть ps — кососферическое множество точек в P. Тогда для любых двух n-мерных симплексов sx1, sx2 с вершинами в ps радиусы их описанных окружностей совпадают.
LaTeX
$$$\exists r \in \mathbb{R},\; \text{∀ sx}_1, \text{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.circumradius = sx_2.circumradius$$$
Lean4
/-- Two n-simplices among cospherical points in n-space have the same
circumradius. -/
theorem circumradius_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₁.circumradius = sx₂.circumradius :=
by
rcases exists_circumradius_eq_of_cospherical hd hc with ⟨r, hr⟩
rw [hr sx₁ hsx₁, hr sx₂ hsx₂]
