congruent_iff_nndist_eq — Mathlib

English

Two indexed families are congruent if and only if all nonnegative distances between corresponding indices agree under the two families.

Русский

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

LaTeX

$$$ \text{Congruent}(v_1,v_2) \iff \forall i_1,i_2,\; \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 are the same. -/
theorem congruent_iff_nndist_eq : Congruent v₁ v₂ ↔ ∀ i₁ i₂, nndist (v₁ i₁) (v₁ i₂) = nndist (v₂ i₁) (v₂ i₂) :=
  forall₂_congr (fun _ _ ↦ by rw [edist_nndist, edist_nndist]; norm_cast)

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