English
If two simplices are cospherical subsets of the same affine subspace, then their circumradii are equal.
Русский
Если два простых многогранника образуют косферическую совокупность внутри одного афинного подпроизвольного пространства, их circumradius равны.
LaTeX
$$$\text{Cospherical}(ps) \land \text{subset relations} \Rightarrow \text{circumradius}(sx_1)=\text{circumradius}(sx_2)$$$
Lean4
/-- Two n-simplices among cospherical points in an n-dimensional
subspace have the same circumradius. -/
theorem circumradius_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₁.circumradius = sx₂.circumradius :=
by
rcases exists_circumradius_eq_of_cospherical_subset h hd hc with ⟨r, hr⟩
rw [hr sx₁ hsx₁, hr sx₂ hsx₂]
