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 #

class DilationEquivClass (F : Type u_1) (X : outParam (Type u_2)) (Y : outParam (Type u_3)) [PseudoEMetricSpace X] [PseudoEMetricSpace Y] extends EquivLike :
Type (max (max u_1 u_2) u_3)

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

      Inverse DilationEquiv.

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

        Instances For

          Identity map as a DilationEquiv.

          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) :
            ↑(DilationEquiv.trans e₁ e₂) = e₂ e₁
            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.

            Instances For
              theorem DilationEquiv.mul_def {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) (e' : X ≃ᵈ X) :
              @[simp]
              theorem DilationEquiv.coe_mul {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) (e' : X ≃ᵈ X) :
              ↑(e * e') = e e'
              @[simp]
              theorem DilationEquiv.coe_one {X : Type u_1} [PseudoEMetricSpace X] :
              1 = id
              noncomputable def DilationEquiv.ratioHom {X : Type u_1} [PseudoEMetricSpace X] :

              Dilation.ratio as a monoid homomorphism.

              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 : ) :
                @[simp]
                theorem DilationEquiv.toPerm_apply {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) :
                DilationEquiv.toPerm e = e.toEquiv

                DilationEquiv.toEquiv as a monoid homomorphism.

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