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.coe_toEquiv {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :
            e.toEquiv = e
            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'
            theorem DilationEquiv.ext_iff {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {e e' : X ≃ᵈ Y} :
            e = e' ∀ (x : X), e x = e' x
            def DilationEquiv.symm {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :
            Y ≃ᵈ X

            Inverse DilationEquiv.

            Equations
              Instances For
                @[simp]
                theorem DilationEquiv.symm_symm {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :
                e.symm.symm = e
                @[simp]
                theorem DilationEquiv.apply_symm_apply {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) (x : Y) :
                e (e.symm x) = x
                @[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
                def DilationEquiv.Simps.symm_apply {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :
                YX

                See Note [custom simps projection].

                Equations
                  Instances For

                    Identity map as a DilationEquiv.

                    Equations
                      Instances For
                        @[simp]
                        @[simp]
                        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) :
                        X ≃ᵈ 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) :
                            (e₁.trans e₂) = e₂ e₁
                            @[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
                            @[simp]
                            theorem DilationEquiv.symm_trans_self {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :
                            @[simp]
                            theorem DilationEquiv.self_trans_symm {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :
                            @[simp]
                            Equations
                              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'
                              @[simp]
                              theorem DilationEquiv.coe_one {X : Type u_1} [PseudoEMetricSpace X] :
                              1 = id
                              theorem DilationEquiv.coe_inv {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) :
                              e⁻¹ = e.symm
                              noncomputable def DilationEquiv.ratioHom {X : Type u_1} [PseudoEMetricSpace X] :

                              Dilation.ratio as a monoid homomorphism.

                              Equations
                                Instances For
                                  @[simp]
                                  theorem DilationEquiv.ratio_pow {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) (n : ) :
                                  @[simp]
                                  theorem DilationEquiv.ratio_zpow {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) (n : ) :

                                  DilationEquiv.toEquiv as a monoid homomorphism.

                                  Equations
                                    Instances For
                                      @[simp]
                                      theorem DilationEquiv.coe_pow {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) (n : ) :
                                      ⇑(e ^ n) = (⇑e)^[n]

                                      Every isometry equivalence is a dilation equivalence of ratio 1.

                                      Equations
                                        Instances For
                                          @[simp]
                                          theorem IsometryEquiv.toDilationEquiv_apply {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵢ Y) (x : X) :

                                          Reinterpret a DilationEquiv as a homeomorphism.

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