similar_iff_exists_dist_eq — Mathlib

English

Similarity is equivalent to existence of a scalar r such that dist(v1 i1, v1 i2) = r · dist(v2 i1, v2 i2) for all i1,i2.

Русский

Сходство эквивалентно существованию множителя r, такого что dist(v1 i1, v1 i2) = r · dist(v2 i1, v2 i2) для всех i1,i2.

LaTeX

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

Lean4

/-- Similarity holds if and only if all distances are proportional. -/
theorem similar_iff_exists_dist_eq :
    Similar v₁ v₂ ↔ (∃ r : ℝ≥0, r ≠ 0 ∧ ∀ (i₁ i₂ : ι), (dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂))) :=
  similar_iff_exists_nndist_eq.trans
    (exists_congr <| fun _ =>
      and_congr Iff.rfl <|
        forall₂_congr <| fun _ _ => by { rw [dist_nndist, dist_nndist]; norm_cast
        })

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