Documentation

Mathlib.Topology.MetricSpace.DilationEquiv

Dilation equivalence #

In this file we define DilationEquiv X Y, a type of bundled equivalences between X and Ysuch thatedist (f x) (f y) = r * edist x yfor somer : ℝ≥0, r ≠ 0`.

We also develop basic API about these equivalences.

TODO #

Typeclass saying that F is a type of bundled equivalences such that all e : F are dilations.

Instances
    structure DilationEquiv (X : Type u_1) (Y : Type u_2) [PseudoEMetricSpace X] [PseudoEMetricSpace Y] extends X Y, X →ᵈ Y :
    Type (max u_1 u_2)

    Type of equivalences X ≃ Y such that ∀ x y, edist (f x) (f y) = r * edist x y for some r : ℝ≥0, r ≠ 0.

    Instances For

      Type of equivalences X ≃ Y such that ∀ x y, edist (f x) (f y) = r * edist x y for some r : ℝ≥0, r ≠ 0.

      Equations
      Instances For
        Equations
        @[simp]
        theorem DilationEquiv.ext {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {e e' : X ≃ᵈ Y} (h : ∀ (x : X), e x = e' x) :
        e = e'

        Inverse DilationEquiv.

        Equations
        Instances For
          @[simp]
          @[simp]
          theorem DilationEquiv.apply_symm_apply {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) (x : Y) :
          @[simp]
          theorem DilationEquiv.symm_apply_apply {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) (x : X) :
          e.symm (e x) = x

          See Note [custom simps projection].

          Equations
          Instances For

            Identity map as a DilationEquiv.

            Equations
            Instances For
              def DilationEquiv.trans {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] [PseudoEMetricSpace Z] (e₁ : X ≃ᵈ Y) (e₂ : Y ≃ᵈ Z) :

              Composition of DilationEquivs.

              Equations
              Instances For
                @[simp]
                theorem DilationEquiv.trans_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] [PseudoEMetricSpace Z] (e₁ : X ≃ᵈ Y) (e₂ : Y ≃ᵈ Z) :
                @[simp]
                theorem DilationEquiv.refl_trans {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :
                (refl X).trans e = e
                @[simp]
                theorem DilationEquiv.trans_refl {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :
                e.trans (refl Y) = e
                theorem DilationEquiv.mul_def {X : Type u_1} [PseudoEMetricSpace X] (e e' : X ≃ᵈ X) :
                e * e' = e'.trans e
                @[simp]
                theorem DilationEquiv.coe_mul {X : Type u_1} [PseudoEMetricSpace X] (e e' : X ≃ᵈ X) :
                (e * e') = e e'

                Dilation.ratio as a monoid homomorphism.

                Equations
                Instances For

                  DilationEquiv.toEquiv as a monoid homomorphism.

                  Equations
                  Instances For

                    Every isometry equivalence is a dilation equivalence of ratio 1.

                    Equations
                    Instances For
                      @[simp]

                      Reinterpret a DilationEquiv as a homeomorphism.

                      Equations
                      Instances For