English
Similarity of two families is characterized by a fixed scalar r > 0 relating all pairwise nonnegative distances via nndist.
Русский
Сходность двух семейств характеризуется постоянным множителем r > 0, который соотносит попарные безотрицательные расстояния через nndist.
LaTeX
$$Similar v1 v2 iff ∃ r > 0 such that Pairwise (i1,i2) ↦ (nndist(v1 i1, v1 i2) = r * nndist(v2 i1, v2 i2)).$$
Lean4
/-- Similarity holds if and only if all extended distances between points with different
indices are proportional. -/
theorem similar_iff_exists_pairwise_edist_eq :
Similar v₁ v₂ ↔ (∃ r : ℝ≥0, r ≠ 0 ∧ Pairwise fun i₁ i₂ ↦ (edist (v₁ i₁) (v₁ i₂) = r * edist (v₂ i₁) (v₂ i₂))) :=
by
rw [similar_iff_exists_edist_eq]
refine ⟨?_, ?_⟩ <;> rintro ⟨r, hr, h⟩ <;> refine ⟨r, hr, fun i₁ i₂ ↦ ?_⟩
· exact fun _ ↦ h i₁ i₂
· by_cases hi : i₁ = i₂
· simp [hi]
· exact h hi
