English
If the orthogonal projection of p onto the span of a simplex equals the circumcenter, then that projection equals the circumcenter.
Русский
Если ортогональная проекция p на пространство, порожденное симплексом, равна circumsphere center, то она равна circumcenter.
LaTeX
$$$\\uparrow( s.orthogonalProjectionSpan p ) = s.circumcenter$ under appropriate dist conditions.$$
Lean4
theorem dist_circumcenter_sq_eq_sq_sub_circumradius {n : ℕ} {r : ℝ} (s : Simplex ℝ P n) {p₁ : P}
(h₁ : ∀ i : Fin (n + 1), dist (s.points i) p₁ = r) (h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter)
(h : s.points 0 ∈ affineSpan ℝ (Set.range s.points)) :
dist p₁ s.circumcenter * dist p₁ s.circumcenter = r * r - s.circumradius * s.circumradius :=
by
rw [dist_comm, ← h₁ 0, s.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq p₁ h]
simp only [h₁', dist_comm p₁, add_sub_cancel_left, Simplex.dist_circumcenter_eq_circumradius]
