English
A simplex is regular if it is equivalent, up to isometry, to any relabeling of its vertices: for every permutation of vertex indices, there exists an ambient isometry mapping the labeled points accordingly.
Русский
Симплекс регулярный, если он равносилен, по изометрии, любому перенумеровaнию вершин: для каждой перестановки индексов вершин существует изометрия пространства, отправляющая вершины в соответствующем порядке.
LaTeX
$$$\forall \sigma : \operatorname{Perm}(\{0,\dots,n\}), \exists x : P \cong_i P,\ s.p \circ \sigma = x \circ s.p$$$
Lean4
@[simp]
theorem equilateral_reindex_iff {s : Simplex R P m} (e : Fin (m + 1) ≃ Fin (n + 1)) :
(s.reindex e).Equilateral ↔ s.Equilateral :=
by
refine ⟨fun ⟨r, hr⟩ ↦ ⟨r, fun i j hij ↦ ?_⟩, fun ⟨r, hr⟩ ↦ ⟨r, fun i j hij ↦ ?_⟩⟩
· convert hr (e i) (e j) (e.injective.ne hij) using 2 <;> simp
· convert hr (e.symm i) (e.symm j) (e.symm.injective.ne hij) using 2
