English
Reindexing along Equiv preserves circumsphere.
Русский
Перебиндирование по эквивалентности сохраняет circumsphere.
LaTeX
$$$(s.reindex e).circumsphere = s.circumsphere$ for any $e$.$$
Lean4
/-- The circumcenter of a 1-simplex equals its centroid. -/
theorem circumcenter_eq_centroid (s : Simplex ℝ P 1) : s.circumcenter = Finset.univ.centroid ℝ s.points :=
by
have hr :
Set.Pairwise Set.univ fun i j : Fin 2 =>
dist (s.points i) (Finset.univ.centroid ℝ s.points) = dist (s.points j) (Finset.univ.centroid ℝ s.points) :=
by
intro i hi j hj hij
rw [Finset.centroid_pair_fin, dist_eq_norm_vsub V (s.points i), dist_eq_norm_vsub V (s.points j),
vsub_vadd_eq_vsub_sub, vsub_vadd_eq_vsub_sub, ← one_smul ℝ (s.points i -ᵥ s.points 0), ←
one_smul ℝ (s.points j -ᵥ s.points 0)]
fin_cases i <;> fin_cases j <;> simp [-one_smul, ← sub_smul] <;> norm_num
rw [Set.pairwise_eq_iff_exists_eq] at hr
obtain ⟨r, hr⟩ := hr
exact
(s.eq_circumcenter_of_dist_eq (centroid_mem_affineSpan_of_card_eq_add_one ℝ _ (Finset.card_fin 2)) fun i =>
hr i (Set.mem_univ _)).symm
