English
Let s be an affine subspace of P and ps a subset of s. If ps is cospherical and hd holds in s, then there exists a point c in P such that every simplex with vertices in ps has circumcenter equal to c.
Русский
Пусть s — аффинное подпространство P, ps ⊆ s. Если ps кососферично и hd выполняется в s, то существует точка c ∈ P, такая что для каждой симплексной фигуры с вершинами в ps её circumcenter совпадает с c.
LaTeX
$$$\exists c \in P, \forall sx : \text{Simplex } \mathbb{R} P\, n,\; (\text{range } sx.points \subseteq ps) \Rightarrow sx.circumcenter = c$$$
Lean4
/-- All n-simplices among cospherical points in an n-dimensional
subspace have the same circumcenter. -/
theorem exists_circumcenter_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 : P, ∀ sx : Simplex ℝ P n, Set.range sx.points ⊆ ps → sx.circumcenter = c :=
by
rw [cospherical_iff_exists_mem_of_finiteDimensional h] at hc
rcases hc with ⟨c, hc, r, hcr⟩
use c
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_circumcenter_of_dist_eq hc fun i => hcr (sx.points i) (hsxps (Set.mem_range_self i))).symm
