English
If there exists a point p with a distance r to all vertices of a simplex, the orthogonal projection of p onto the affine span of the simplex is the circumcenter.
Русский
Если существует точка p с расстоянием r до всех вершин множества, ортогональная проекция p на афинное пространство симплексa — это циркумцентр.
LaTeX
$$$\\exists r\\; \\forall i, dist (s.points i) p = r \\Rightarrow ↑(s.orthogonalProjectionSpan p) = s.circumcenter$$$
Lean4
/-- If there exists a distance that a point has from all vertices of a
simplex, the orthogonal projection of that point onto the subspace
spanned by that simplex is its circumcenter. -/
theorem orthogonalProjection_eq_circumcenter_of_exists_dist_eq {n : ℕ} (s : Simplex ℝ P n) {p : P}
(hr : ∃ r, ∀ i, dist (s.points i) p = r) : ↑(s.orthogonalProjectionSpan p) = s.circumcenter :=
by
change ∃ r : ℝ, ∀ i, (fun x => dist x p = r) (s.points i) at hr
have hr : ∃ (r : ℝ), ∀ (a : P), a ∈ Set.range (fun (i : Fin (n + 1)) => s.points i) → dist a p = r :=
by
obtain ⟨r, hr⟩ := hr
use r
refine Set.forall_mem_range.mpr ?_
exact hr
rw [exists_dist_eq_iff_exists_dist_orthogonalProjection_eq (subset_affineSpan ℝ _) p] at hr
obtain ⟨r, hr⟩ := hr
exact s.eq_circumcenter_of_dist_eq (orthogonalProjection_mem p) fun i => hr _ (Set.mem_range_self i)
