congruent_iff_dist_eq — Mathlib

English

Two indexed families are congruent if and only if all pairwise distances between their images match.

Русский

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

LaTeX

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

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