English
Two simplices with the same vertex set have the same circumcenter.
Русский
Два простых многогранника, имеющих один и тот же набор вершин, имеют один и тот же центр описанной окружности.
LaTeX
$$$\text{If }\mathrm{range}(s_1.points)=\mathrm{range}(s_2.points),\; s_1.circumcenter = s_2.circumcenter$$$
Lean4
/-- Two simplices with the same points have the same circumcenter. -/
theorem circumcenter_eq_of_range_eq {n : ℕ} {s₁ s₂ : Simplex ℝ P n} (h : Set.range s₁.points = Set.range s₂.points) :
s₁.circumcenter = s₂.circumcenter :=
by
have hs : s₁.circumcenter ∈ affineSpan ℝ (Set.range s₂.points) := h ▸ s₁.circumcenter_mem_affineSpan
have hr : ∀ i, dist (s₂.points i) s₁.circumcenter = s₁.circumradius :=
by
intro i
have hi : s₂.points i ∈ Set.range s₂.points := Set.mem_range_self _
rw [← h, Set.mem_range] at hi
rcases hi with ⟨j, hj⟩
rw [← hj, s₁.dist_circumcenter_eq_circumradius j]
exact s₂.eq_circumcenter_of_dist_eq hs hr
