congruent_iff_pairwise_dist_eq — Mathlib

English

Two families are congruent if and only if all pairwise distances are equal, with respect to the metric.

Русский

Два семейства согласованы тогда и только тогда, когда все попарные расстояния совпадают.

LaTeX

$$$ \text{Congruent}(v_1,v_2) \iff \text{Pairwise }(i_1,i_2 \mapsto \mathrm{dist}(v_1(i_1),v_1(i_2)) = \mathrm{dist}(v_2(i_1),v_2(i_2))).$$$

Lean4

/-- Congruence holds if and only if all non-negative distances between points with different
indices are the same. -/
theorem congruent_iff_pairwise_dist_eq :
    Congruent v₁ v₂ ↔ Pairwise fun i₁ i₂ ↦ dist (v₁ i₁) (v₁ i₂) = dist (v₂ i₁) (v₂ i₂) :=
  by
  simp_rw [congruent_iff_pairwise_nndist_eq, dist_nndist]
  exact_mod_cast Iff.rfl

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