equilateral_iff_dist_01_eq_02_and_dist_01_eq_12

English

If s is equilateral, then for any i1,i2,i3,i4 with i1 ≠ i2 and i3 ≠ i4, the distances are equal for all pairs.

Русский

Если симплекс равносторонний, то расстояния между любыми парами вершин равны.

LaTeX

$$$\forall i_1,i_2,i_3,i_4,\ i_1 \neq i_2 \land i_3 \neq i_4 \Rightarrow \operatorname{dist}(s.p(i_1), s.p(i_2)) = \operatorname{dist}(s.p(i_3), s.p(i_4)).$$$

Lean4

theorem equilateral_iff_dist_01_eq_02_and_dist_01_eq_12 {t : Triangle R P} :
    t.Equilateral ↔
      dist (t.points 0) (t.points 1) = dist (t.points 0) (t.points 2) ∧
        dist (t.points 0) (t.points 1) = dist (t.points 1) (t.points 2) :=
  equilateral_iff_dist_eq_and_dist_eq (by decide) (by decide) (by decide)

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