similar_iff_exists_pairwise_nndist_eq

English

Similarity holds iff all pairwise distances are proportional by a single scalar r > 0.

Русский

Сходство достигается тогда и только тогда, когда все попарные расстояния пропорциональны одной константе r > 0.

LaTeX

$$Similar v1 v2 ↔ ∃ r>0, Pairwise (i1,i2) ↦ dist(v1 i1, v1 i2) = r · dist(v2 i1, v2 i2).$$

Lean4

/-- Similarity holds if and only if all non-negative distances between points with different
indices are proportional. -/
theorem similar_iff_exists_pairwise_nndist_eq :
    Similar v₁ v₂ ↔ (∃ r : ℝ≥0, r ≠ 0 ∧ Pairwise fun i₁ i₂ ↦ (nndist (v₁ i₁) (v₁ i₂) = r * nndist (v₂ i₁) (v₂ i₂))) :=
  by
  simp_rw [similar_iff_exists_pairwise_edist_eq, edist_nndist]
  exact_mod_cast Iff.rfl

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