Equilateral — Mathlib

English

If s is equilateral, then all three pairwise distances are equal: dist(s.p(0), s.p(1)) = dist(s.p(0), s.p(2)) and dist(s.p(0), s.p(1)) = dist(s.p(1), s.p(2)).

Русский

Если симплекс равносторонний, то три расстояния между парами вершин равны: dist(0,1) = dist(0,2) = dist(1,2).

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))$ for all i1,i2,i3,i4 с i1 ≠ i2, i3 ≠ i4.$$

Lean4

/-- A simplex is equilateral if all the edge lengths are equal. -/
def Equilateral (s : Simplex R P n) : Prop :=
  ∃ r : ℝ, ∀ i j, i ≠ j → dist (s.points i) (s.points j) = r

Похожие утверждения