congruent_iff_pairwise_nndist_eq — Mathlib

English

A congruence between v1 and v2 is equivalent to the pairwise equality of nonnegative distances for all index pairs.

Русский

Согласованность между v1 и v2 эквивалентна попарному равенству неотрицательных расстояний для всех пар индексов.

LaTeX

$$$ \text{Congruent}(v_1,v_2) \iff \text{Pairwise }(i_1,i_2 \mapsto \mathrm{nndist}(v_1(i_1),v_1(i_2)) = \mathrm{nndist}(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_nndist_eq :
    Congruent v₁ v₂ ↔ Pairwise fun i₁ i₂ ↦ nndist (v₁ i₁) (v₁ i₂) = nndist (v₂ i₁) (v₂ i₂) :=
  by
  simp_rw [congruent_iff_pairwise_edist_eq, edist_nndist]
  exact_mod_cast Iff.rfl

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