English
All n-simplices among cospherical points in an n-dimensional subspace admit a common circumradius; i.e., there exists r such that all simplices in the family have circumradius r.
Русский
Все n-мерные простые многогранники среди кососферных точек в n-мерном подпроекте имеют общий circumradius; т.е. существует r, такой что все простые многогранники в семье имеют circumradius r.
LaTeX
$$$\exists r\, \forall sx\, (hsx\,subset\; ps) \; (sx.circumradius = r)$$$
Lean4
/-- Given a nonempty affine subspace, whose direction is complete,
that contains a set of points, those points are cospherical if and
only if they are equidistant from some point in that subspace. -/
theorem cospherical_iff_exists_mem_of_complete {s : AffineSubspace ℝ P} {ps : Set P} (h : ps ⊆ s) [Nonempty s]
[s.direction.HasOrthogonalProjection] :
Cospherical ps ↔ ∃ center ∈ s, ∃ radius : ℝ, ∀ p ∈ ps, dist p center = radius :=
by
constructor
· rintro ⟨c, hcr⟩
rw [exists_dist_eq_iff_exists_dist_orthogonalProjection_eq h c] at hcr
exact ⟨orthogonalProjection s c, orthogonalProjection_mem _, hcr⟩
· exact fun ⟨c, _, hd⟩ => ⟨c, hd⟩
