Documentation

Mathlib.Topology.MetricSpace.Congruence

Congruences #

This file defines Congruent, i.e., the equivalence between indexed families of points in a metric space where all corresponding pairwise distances are the same. The motivating example are triangles in the plane.

Implementation notes #

After considering two possible approaches to defining congruence — either based on equal pairwise distances or the existence of an isometric equivalence — we have opted for the broader concept of equal pairwise distances. This notion is commonly employed in the literature across various metric spaces that lack an isometric equivalence.

For more details see the Zulip discussion.

Notation #

source
def Congruent {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} [PseudoEMetricSpace P₁] [PseudoEMetricSpace P₂] (v₁ : ι → P₁) (v₂ : ι → P₂) :
Prop

A congruence between indexed sets of vertices v₁ and v₂. Use open scoped Congruent to access the v₁ ≅ v₂ notation.

Equations
  • Congruent v₁ v₂ = ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
Instances For
    source
    def Congruent.«term_≅_» :
    Lean.TrailingParserDescr

    A congruence between indexed sets of vertices v₁ and v₂. Use open scoped Congruent to access the v₁ ≅ v₂ notation.

    Equations
    Instances For
      source
      theorem congruent_iff_edist_eq {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [PseudoEMetricSpace P₁] [PseudoEMetricSpace P₂] :
      Congruent v₁ v₂ ↔ ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)

      Congruence holds if and only if all extended distances are the same.

      source
      theorem congruent_iff_pairwise_edist_eq {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [PseudoEMetricSpace P₁] [PseudoEMetricSpace P₂] :
      Congruent v₁ v₂ ↔ Pairwise fun (i₁ i₂ : ι) => edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)

      Congruence holds if and only if all extended distances between points with different indices are the same.

      source
      theorem Congruent.edist_eq {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [PseudoEMetricSpace P₁] [PseudoEMetricSpace P₂] :
      Congruent v₁ v₂ → ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)

      A congruence preserves extended distance. Forward direction of congruent_iff_edist_eq.

      source
      theorem Congruent.of_edist_eq {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [PseudoEMetricSpace P₁] [PseudoEMetricSpace P₂] :
      (∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)) → Congruent v₁ v₂

      Congruence follows from preserved extended distance. Backward direction of congruent_iff_edist_eq.

      source
      theorem Congruent.pairwise_edist_eq {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [PseudoEMetricSpace P₁] [PseudoEMetricSpace P₂] :
      Congruent v₁ v₂ → Pairwise fun (i₁ i₂ : ι) => edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)

      A congruence pairwise preserves extended distance. Forward direction of congruent_iff_pairwise_edist_eq.

      source
      theorem Congruent.of_pairwise_edist_eq {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [PseudoEMetricSpace P₁] [PseudoEMetricSpace P₂] :
      (Pairwise fun (i₁ i₂ : ι) => edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)) → Congruent v₁ v₂

      Congruence follows from pairwise preserved extended distance. Backward direction of congruent_iff_pairwise_edist_eq.

      source
      theorem Congruent.refl {ι : Type u_1} {P₁ : Type u_3} [PseudoEMetricSpace P₁] (v₁ : ι → P₁) :
      Congruent v₁ v₁
      source
      theorem Congruent.symm {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [PseudoEMetricSpace P₁] [PseudoEMetricSpace P₂] (h : Congruent v₁ v₂) :
      Congruent v₂ v₁
      source
      theorem congruent_comm {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [PseudoEMetricSpace P₁] [PseudoEMetricSpace P₂] :
      Congruent v₁ v₂ ↔ Congruent v₂ v₁
      source
      theorem Congruent.trans {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {P₃ : Type u_5} {v₁ : ι → P₁} {v₂ : ι → P₂} {v₃ : ι → P₃} [PseudoEMetricSpace P₁] [PseudoEMetricSpace P₂] [PseudoEMetricSpace P₃] (h₁₂ : Congruent v₁ v₂) (h₂₃ : Congruent v₂ v₃) :
      Congruent v₁ v₃
      source
      theorem Congruent.index_map {ι : Type u_1} {ι' : Type u_2} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [PseudoEMetricSpace P₁] [PseudoEMetricSpace P₂] (h : Congruent v₁ v₂) (f : ι' → ι) :
      Congruent (v₁ ∘ f) (v₂ ∘ f)

      Change the index set ι to an index ι' that maps to ι.

      source
      @[simp]
      theorem Congruent.index_equiv {ι : Type u_1} {ι' : Type u_2} {P₁ : Type u_3} {P₂ : Type u_4} [PseudoEMetricSpace P₁] [PseudoEMetricSpace P₂] {E : Type u_6} [EquivLike E ι' ι] (f : E) (v₁ : ι → P₁) (v₂ : ι → P₂) :
      Congruent (v₁ ∘ ⇑f) (v₂ ∘ ⇑f) ↔ Congruent v₁ v₂

      Change between equivalent index sets ι and ι'.

      source
      theorem congruent_iff_nndist_eq {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [PseudoMetricSpace P₁] [PseudoMetricSpace P₂] :
      Congruent v₁ v₂ ↔ ∀ (i₁ i₂ : ι), nndist (v₁ i₁) (v₁ i₂) = nndist (v₂ i₁) (v₂ i₂)

      Congruence holds if and only if all non-negative distances are the same.

      source
      theorem congruent_iff_pairwise_nndist_eq {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [PseudoMetricSpace P₁] [PseudoMetricSpace P₂] :
      Congruent v₁ v₂ ↔ Pairwise fun (i₁ i₂ : ι) => nndist (v₁ i₁) (v₁ i₂) = nndist (v₂ i₁) (v₂ i₂)

      Congruence holds if and only if all non-negative distances between points with different indices are the same.

      source
      theorem congruent_iff_dist_eq {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [PseudoMetricSpace P₁] [PseudoMetricSpace P₂] :
      Congruent v₁ v₂ ↔ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = dist (v₂ i₁) (v₂ i₂)

      Congruence holds if and only if all distances are the same.

      source
      theorem congruent_iff_pairwise_dist_eq {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [PseudoMetricSpace P₁] [PseudoMetricSpace P₂] :
      Congruent v₁ v₂ ↔ Pairwise fun (i₁ i₂ : ι) => dist (v₁ i₁) (v₁ i₂) = dist (v₂ i₁) (v₂ i₂)

      Congruence holds if and only if all non-negative distances between points with different indices are the same.

      source
      theorem Congruent.nndist_eq {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [PseudoMetricSpace P₁] [PseudoMetricSpace P₂] :
      Congruent v₁ v₂ → ∀ (i₁ i₂ : ι), nndist (v₁ i₁) (v₁ i₂) = nndist (v₂ i₁) (v₂ i₂)

      A congruence preserves non-negative distance. Forward direction of congruent_iff_nndist_eq.

      source
      theorem Congruent.of_nndist_eq {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [PseudoMetricSpace P₁] [PseudoMetricSpace P₂] :
      (∀ (i₁ i₂ : ι), nndist (v₁ i₁) (v₁ i₂) = nndist (v₂ i₁) (v₂ i₂)) → Congruent v₁ v₂

      Congruence follows from preserved non-negative distance. Backward direction of congruent_iff_nndist_eq.

      source
      theorem Congruent.dist_eq {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [PseudoMetricSpace P₁] [PseudoMetricSpace P₂] :
      Congruent v₁ v₂ → ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = dist (v₂ i₁) (v₂ i₂)

      A congruence preserves distance. Forward direction of congruent_iff_dist_eq.

      source
      theorem Congruent.of_dist_eq {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [PseudoMetricSpace P₁] [PseudoMetricSpace P₂] :
      (∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = dist (v₂ i₁) (v₂ i₂)) → Congruent v₁ v₂

      Congruence follows from preserved distance. Backward direction of congruent_iff_dist_eq.

      source
      theorem Congruent.pairwise_nndist_eq {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [PseudoMetricSpace P₁] [PseudoMetricSpace P₂] :
      Congruent v₁ v₂ → Pairwise fun (i₁ i₂ : ι) => nndist (v₁ i₁) (v₁ i₂) = nndist (v₂ i₁) (v₂ i₂)

      A congruence pairwise preserves non-negative distance. Forward direction of congruent_iff_pairwise_nndist_eq.

      source
      theorem Congruent.of_pairwise_nndist_eq {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [PseudoMetricSpace P₁] [PseudoMetricSpace P₂] :
      (Pairwise fun (i₁ i₂ : ι) => nndist (v₁ i₁) (v₁ i₂) = nndist (v₂ i₁) (v₂ i₂)) → Congruent v₁ v₂

      Congruence follows from pairwise preserved non-negative distance. Backward direction of congruent_iff_pairwise_nndist_eq.

      source
      theorem Congruent.pairwise_dist_eq {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [PseudoMetricSpace P₁] [PseudoMetricSpace P₂] :
      Congruent v₁ v₂ → Pairwise fun (i₁ i₂ : ι) => dist (v₁ i₁) (v₁ i₂) = dist (v₂ i₁) (v₂ i₂)

      A congruence pairwise preserves distance. Forward direction of congruent_iff_pairwise_dist_eq.

      source
      theorem Congruent.of_pairwise_dist_eq {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [PseudoMetricSpace P₁] [PseudoMetricSpace P₂] :
      (Pairwise fun (i₁ i₂ : ι) => dist (v₁ i₁) (v₁ i₂) = dist (v₂ i₁) (v₂ i₂)) → Congruent v₁ v₂

      Congruence follows from pairwise preserved distance. Backward direction of congruent_iff_pairwise_dist_eq.