Similarities #
This file defines Similar, i.e., the equivalence between indexed sets of points in a metric space
where all corresponding pairwise distances have the same ratio. The motivating example is
triangles in the plane.
Implementation notes #
For more details see the Zulip discussion.
Notation #
Let P₁ and P₂ be metric spaces, let ι be an index set, and let v₁ : ι → P₁ and
v₂ : ι → P₂ be indexed families of points.
(v₁ ∼ v₂ : Prop)represents that(v₁ : ι → P₁)and(v₂ : ι → P₂)are similar.
Similarity between indexed sets of vertices v₁ and v₂.
Use open scoped Similar to access the v₁ ∼ v₂ notation.
Equations
Instances For
Similarity between indexed sets of vertices v₁ and v₂.
Use open scoped Similar to access the v₁ ∼ v₂ notation.
Equations
- Similar.«term_∼_» = Lean.ParserDescr.trailingNode `Similar.«term_∼_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∼ ") (Lean.ParserDescr.cat `term 26))
Instances For
Similarity holds if and only if all extended distances are proportional.
Similarity holds if and only if all extended distances between points with different indices are proportional.
A similarity scales extended distance. Forward direction of similar_iff_exists_edist_eq.
Similarity follows from scaled extended distance. Backward direction of
similar_iff_exists_edist_eq.
A similarity pairwise scales extended distance. Forward direction of
similar_iff_exists_pairwise_edist_eq.
Similarity follows from pairwise scaled extended distance. Backward direction of
similar_iff_exists_pairwise_edist_eq.
Change the index set ι to an index ι' that maps to ι.
Change between equivalent index sets ι and ι'.
Similarity holds if and only if all non-negative distances are proportional.
Similarity holds if and only if all non-negative distances between points with different indices are proportional.
Similarity holds if and only if all distances are proportional.
Similarity holds if and only if all distances between points with different indices are proportional.
A similarity scales non-negative distance. Forward direction of
similar_iff_exists_nndist_eq.
Similarity follows from scaled non-negative distance. Backward direction of
similar_iff_exists_nndist_eq.
A similarity scales distance. Forward direction of similar_iff_exists_dist_eq.
Similarity follows from scaled distance. Backward direction of
similar_iff_exists_dist_eq.
A similarity pairwise scales non-negative distance. Forward direction of
similar_iff_exists_pairwise_nndist_eq.
Similarity follows from pairwise scaled non-negative distance. Backward direction of
similar_iff_exists_pairwise_nndist_eq.
A similarity pairwise scales distance. Forward direction of
similar_iff_exists_pairwise_dist_eq.
Similarity follows from pairwise scaled distance. Backward direction of
similar_iff_exists_pairwise_dist_eq.