English
Similarity is equivalent to the existence of a positive scalar r relating all pairwise distances by dist(v1 i1, v1 i2) = r · dist(v2 i1, v2 i2).
Русский
Сходство эквивалентно существованию положительного множителя r, который относит попарные расстояния по v1 и v2: dist(v1 i1, v1 i2) = r · dist(v2 i1, v2 i2).
LaTeX
$$$ Similar(v_1,v_2) \\iff \\exists r>0, \\forall i_1,i_2, dist(v_1 i_1, v_1 i_2) = r \\cdot dist(v_2 i_1, v_2 i_2). $$$
Lean4
/-- Similarity holds if and only if all non-negative distances are proportional. -/
theorem similar_iff_exists_nndist_eq :
Similar v₁ v₂ ↔ (∃ r : ℝ≥0, r ≠ 0 ∧ ∀ (i₁ i₂ : ι), (nndist (v₁ i₁) (v₁ i₂) = r * nndist (v₂ i₁) (v₂ i₂))) :=
exists_congr <| fun _ =>
and_congr Iff.rfl <|
forall₂_congr <| fun _ _ => by { rw [edist_nndist, edist_nndist]; norm_cast
}
