English
If ps is a subset of an affine subspace s and the subspace has finite dimension or completeness, cosphericality is characterized by existence of a center in s with equal distances to all points.
Русский
Если ps подмножество s, а подпроизвольная часть имеет конечную размерность, косферичность определяется существованием центра в s с одинаковыми расстояниями до всех точек ps.
LaTeX
$$$\text{Cospherical}(ps) \Rightarrow \exists c\in s, \exists r, \forall p\in ps, \ dist(p,c)=r$$$
Lean4
/-- All n-simplices among cospherical points in an n-dimensional
subspace have the same circumradius. -/
theorem exists_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) :
∃ r : ℝ, ∀ sx : Simplex ℝ P n, Set.range sx.points ⊆ ps → sx.circumradius = r :=
by
rw [cospherical_iff_exists_mem_of_finiteDimensional h] at hc
rcases hc with ⟨c, hc, r, hcr⟩
use r
intro sx hsxps
have hsx : affineSpan ℝ (Set.range sx.points) = s :=
by
refine
sx.independent.affineSpan_eq_of_le_of_card_eq_finrank_add_one (affineSpan_le_of_subset_coe (hsxps.trans h)) ?_
simp [hd]
have hc : c ∈ affineSpan ℝ (Set.range sx.points) := hsx.symm ▸ hc
exact (sx.eq_circumradius_of_dist_eq hc fun i => hcr (sx.points i) (hsxps (Set.mem_range_self i))).symm
