English
From Regular, deduce Equilateral: all pairwise distances between distinct vertices are equal.
Русский
Из Регулярного следует, что расстояния между любыми парами вершины равны.
LaTeX
$$$\text{Regular}(s) \Rightarrow \exists r, \forall i \neq j, \operatorname{dist}(s.p(i), s.p(j)) = r$$$
Lean4
theorem equilateral {s : Simplex R P n} (hr : s.Regular) : s.Equilateral :=
by
refine ⟨dist (s.points 0) (s.points 1), fun i j hij ↦ ?_⟩
have hn : n ≠ 0 := by omega
by_cases hi : i = 1
· rw [hi, dist_comm]
rcases hr (Equiv.swap 0 j) with ⟨x, hx⟩
nth_rw 2 [← x.dist_eq]
simp_rw [← Function.comp_apply (f := x), ← hx]
simp only [comp_apply, Equiv.swap_apply_left]
convert rfl
rw [Equiv.swap_apply_of_ne_of_ne (by simp [hn]) (by cutsat)]
· rcases hr ((Equiv.swap 0 i).trans (Equiv.swap 1 j)) with ⟨x, hx⟩
nth_rw 2 [← x.dist_eq]
simp_rw [← Function.comp_apply (f := x), ← hx]
simp only [Equiv.coe_trans, comp_apply, Equiv.swap_apply_left]
convert rfl
· exact Equiv.swap_apply_of_ne_of_ne hi hij
· rw [Equiv.swap_apply_of_ne_of_ne (by simp [hn]) (Ne.symm hi)]
simp
