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
    theorem DilationEquivClass.edist_eq' {F : Type u_1} {X : outParam (Type u_2)} {Y : outParam (Type u_3)} :
    ∀ {inst : PseudoEMetricSpace X} {inst_1 : PseudoEMetricSpace Y} {inst_2 : EquivLike F X Y} [self : DilationEquivClass F X Y] (f : F), ∃ (r : NNReal), r 0 ∀ (x y : X), edist (f x) (f y) = r * edist x y
    @[instance 100]
    Equations
    • =
    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
      Equations
      • DilationEquiv.instEquivLike = { coe := fun (f : X ≃ᵈ Y) => f.toEquiv, inv := fun (f : X ≃ᵈ Y) => f.symm, left_inv := , right_inv := , coe_injective' := }
      @[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_iff {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {e : X ≃ᵈ Y} {e' : X ≃ᵈ Y} :
      e = e' ∀ (x : X), e x = e' x
      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.

      Equations
      • e.symm = { toEquiv := e.symm, edist_eq' := }
      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]
            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₁
            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
            • e₁.trans e₂ = { toEquiv := e₁.trans e₂.toEquiv, edist_eq' := }
            Instances For
              @[simp]
              theorem DilationEquiv.refl_trans {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :
              (DilationEquiv.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 (DilationEquiv.refl Y) = e
              @[simp]
              theorem DilationEquiv.symm_trans_self {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :
              e.symm.trans e = DilationEquiv.refl Y
              @[simp]
              theorem DilationEquiv.self_trans_symm {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :
              e.trans e.symm = DilationEquiv.refl X
              @[simp]
              theorem DilationEquiv.ratio_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) :
              Equations
              theorem DilationEquiv.mul_def {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) (e' : X ≃ᵈ X) :
              e * e' = e'.trans e
              theorem DilationEquiv.inv_def {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) :
              e⁻¹ = e.symm
              @[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
              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
              • DilationEquiv.ratioHom = { toFun := Dilation.ratio, map_one' := , map_mul' := }
              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.

                Equations
                • DilationEquiv.toPerm = { toFun := fun (e : X ≃ᵈ X) => e.toEquiv, map_one' := , map_mul' := }
                Instances For
                  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
                  • e.toDilationEquiv = { toEquiv := e.toEquiv, edist_eq' := }
                  Instances For
                    @[simp]
                    theorem IsometryEquiv.toDilationEquiv_apply {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵢ Y) (x : X) :
                    e.toDilationEquiv x = e x
                    @[simp]
                    theorem IsometryEquiv.toDilationEquiv_symm {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵢ Y) :
                    e.toDilationEquiv.symm = e.symm.toDilationEquiv
                    @[simp]
                    theorem IsometryEquiv.toDilationEquiv_toDilation {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵢ Y) :
                    e.toDilationEquiv.toDilation = Isometry.toDilation e
                    @[simp]
                    theorem IsometryEquiv.toDilationEquiv_ratio {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵢ Y) :
                    Dilation.ratio e.toDilationEquiv = 1

                    Reinterpret a DilationEquiv as a homeomorphism.

                    Equations
                    • e.toHomeomorph = { toEquiv := e.toEquiv, continuous_toFun := , continuous_invFun := }
                    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
                      @[simp]
                      theorem DilationEquiv.toHomeomorph_symm {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :
                      e.toHomeomorph.symm = e.symm.toHomeomorph