English
Let s be a simplex in an inner product space. If a point p is at equal distance r from every vertex of s, then the orthogonal projection of p onto the affine span of s is the circumcenter of s.
Русский
Пусть s — простой многогранник в пространстве с скалярным произведением. Если точка p находится на одинаковом расстоянии r от всех вершин s, то ортогональная проекция p на афинное пространство, порождаемое вершинами s, есть circumcenter(s).
LaTeX
$$$\forall s\, \forall p\forall r\,\biggl(\forall i,\ \mathrm{dist}(s.points\,i, p)=r\biggr) \Rightarrow s.orthogonalProjectionSpan(p)=s.circumcenter$$$
Lean4
/-- If a point has the same distance 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_dist_eq {n : ℕ} (s : Simplex ℝ P n) {p : P} {r : ℝ}
(hr : ∀ i, dist (s.points i) p = r) : ↑(s.orthogonalProjectionSpan p) = s.circumcenter :=
s.orthogonalProjection_eq_circumcenter_of_exists_dist_eq ⟨r, hr⟩
