English
If s is equilateral, then all edge lengths are equal; hence for any i1,i2,i3,i4 with i1 ≠ i2 and i3 ≠ i4, dist(s.p(i1), s.p(i2)) = dist(s.p(i3), s.p(i4)).
Русский
Если симплекс равносторонний, то все длины рёбер равны; следовательно, для любых ребер расстояния равны.
LaTeX
$$$\text{If } s \text{ is equilateral, then } \operatorname{dist}(s.p(i_1), s.p(i_2)) = \operatorname{dist}(s.p(i_3), s.p(i_4))$$$
Lean4
@[simp]
theorem scalene_reindex_iff {s : Simplex R P m} (e : Fin (m + 1) ≃ Fin (n + 1)) : (s.reindex e).Scalene ↔ s.Scalene :=
by
let f : { x : Fin (m + 1) × Fin (m + 1) // x.1 < x.2 } ≃ { y : Fin (n + 1) × Fin (n + 1) // y.1 < y.2 } :=
⟨fun x ↦
if h : e x.val.1 < e x.val.2 then ⟨(e x.val.1, e x.val.2), h⟩
else ⟨(e x.val.2, e x.val.1), Ne.lt_of_le (e.injective.ne x.property.ne') (not_lt.1 h)⟩,
fun y ↦
if h : e.symm y.val.1 < e.symm y.val.2 then ⟨(e.symm y.val.1, e.symm y.val.2), h⟩
else ⟨(e.symm y.val.2, e.symm y.val.1), Ne.lt_of_le (e.symm.injective.ne y.property.ne') (not_lt.1 h)⟩,
by
simp only [LeftInverse, Subtype.forall, Prod.forall]
intro i j h
split_ifs with h₁ h₂ h₃
· simp
· simp [h] at h₂
· simp [h, lt_asymm] at h₃
· simp, by
simp only [RightInverse, LeftInverse, Subtype.forall, Prod.forall]
intro i j h
split_ifs with h₁ h₂ h₃
· simp
· simp [h] at h₂
· simp [h, lt_asymm] at h₃
· simp⟩
simp_rw [Scalene]
convert (Injective.of_comp_iff' _ (Equiv.bijective f)).symm
simp only [reindex_points, comp_apply, Equiv.coe_fn_mk, f]
split_ifs with h
· simp
· simp [dist_comm]
