dist_eq — Mathlib

English

For any equilateral simplex s, there exists a single length r such that all edges have length r.

Русский

Для любого равностороннего симплекса существует единая длина r, такая что все рёбра имеют длину r.

LaTeX

$$$\exists r \in \mathbb{R}, \forall i \neq j, \operatorname{dist}(s.p(i), s.p(j)) = r$$$

Lean4

theorem dist_eq {s : Simplex R P n} (he : s.Equilateral) {i₁ i₂ i₃ i₄ : Fin (n + 1)} (h₁₂ : i₁ ≠ i₂) (h₃₄ : i₃ ≠ i₄) :
    dist (s.points i₁) (s.points i₂) = dist (s.points i₃) (s.points i₄) :=
  by
  rcases he with ⟨r, hr⟩
  rw [hr _ _ h₁₂, hr _ _ h₃₄]

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