English
All n-simplices among cospherical points in an n-dimensional subspace have the same circumsphere.
Русский
Все n-мерные симплексы с кососферическими точками внутри n-мерного подпространства имеют одну и ту же circumsphere.
LaTeX
$$$\exists c \in \text{Sphere } P, \forall \text{sx} : \text{Simplex } \mathbb{R} P\, n,\; (\text{range } sx.points \subseteq ps) \Rightarrow sx.circumsphere = c$$$
Lean4
/-- All n-simplices among cospherical points in an n-dimensional
subspace have the same circumsphere. -/
theorem exists_circumsphere_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) :
∃ c : Sphere P, ∀ sx : Simplex ℝ P n, Set.range sx.points ⊆ ps → sx.circumsphere = c :=
by
obtain ⟨r, hr⟩ := exists_circumradius_eq_of_cospherical_subset h hd hc
obtain ⟨c, hc⟩ := exists_circumcenter_eq_of_cospherical_subset h hd hc
exact ⟨⟨c, r⟩, fun sx hsx => Sphere.ext (hc sx hsx) (hr sx hsx)⟩
