English
A simplex is scalene if all its edge lengths are pairwise distinct; equivalently, the map from unordered vertex pairs to edge lengths is injective.
Русский
Скалeнный симплекс — это симплекс, для которого длины всех рёбер попарно различны; эквивалентно инъективности отображения пары вершин в длину ребра.
LaTeX
$$$\mathrm{Scalene}(s) = \mathrm{Injective}\Bigl( \lambda e : \{ x : \mathrm{Fin}(n+1) \times \mathrm{Fin}(n+1) \mid x.1 < x.2 \} \mapsto \operatorname{dist}(s.p(x.1), s.p(x.2)) \Bigr)$$$
Lean4
/-- A simplex is scalene if all the edge lengths are different. -/
def Scalene (s : Simplex R P n) : Prop :=
Injective fun i : { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 } ↦ dist (s.points i.val.1) (s.points i.val.2)
