Documentation

Mathlib.Topology.MetricSpace.IsometricSMul

Group actions by isometries #

In this file we define two typeclasses:

We also prove basic facts about isometric actions and define bundled isometries IsometryEquiv.constSMul, IsometryEquiv.mulLeft, IsometryEquiv.mulRight, IsometryEquiv.divLeft, IsometryEquiv.divRight, and IsometryEquiv.inv, as well as their additive versions.

If G is a group, then IsometricSMul G G means that G has a left-invariant metric while IsometricSMul Gᵐᵒᵖ G means that G has a right-invariant metric. For a commutative group, these two notions are equivalent. A group with a right-invariant metric can be also represented as a NormedGroup.

class IsometricVAdd (M : Type u) (X : Type w) [PseudoEMetricSpace X] [VAdd M X] :

An additive action is isometric if each map x ↦ c +ᵥ x is an isometry.

Instances
    class IsometricSMul (M : Type u) (X : Type w) [PseudoEMetricSpace X] [SMul M X] :

    A multiplicative action is isometric if each map x ↦ c • x is an isometry.

    Instances
      theorem isometry_vadd {M : Type u} (X : Type w) [PseudoEMetricSpace X] [VAdd M X] [IsometricVAdd M X] (c : M) :
      Isometry fun x => c +ᵥ x
      theorem isometry_smul {M : Type u} (X : Type w) [PseudoEMetricSpace X] [SMul M X] [IsometricSMul M X] (c : M) :
      Isometry fun x => c x
      @[simp]
      theorem edist_vadd_left {M : Type u} {X : Type w} [PseudoEMetricSpace X] [VAdd M X] [IsometricVAdd M X] (c : M) (x : X) (y : X) :
      edist (c +ᵥ x) (c +ᵥ y) = edist x y
      @[simp]
      theorem edist_smul_left {M : Type u} {X : Type w} [PseudoEMetricSpace X] [SMul M X] [IsometricSMul M X] (c : M) (x : X) (y : X) :
      edist (c x) (c y) = edist x y
      @[simp]
      theorem ediam_vadd {M : Type u} {X : Type w} [PseudoEMetricSpace X] [VAdd M X] [IsometricVAdd M X] (c : M) (s : Set X) :
      @[simp]
      theorem ediam_smul {M : Type u} {X : Type w} [PseudoEMetricSpace X] [SMul M X] [IsometricSMul M X] (c : M) (s : Set X) :
      theorem isometry_add_left {M : Type u} [Add M] [PseudoEMetricSpace M] [IsometricVAdd M M] (a : M) :
      Isometry ((fun x x_1 => x + x_1) a)
      theorem isometry_mul_left {M : Type u} [Mul M] [PseudoEMetricSpace M] [IsometricSMul M M] (a : M) :
      Isometry ((fun x x_1 => x * x_1) a)
      @[simp]
      theorem edist_add_left {M : Type u} [Add M] [PseudoEMetricSpace M] [IsometricVAdd M M] (a : M) (b : M) (c : M) :
      edist (a + b) (a + c) = edist b c
      @[simp]
      theorem edist_mul_left {M : Type u} [Mul M] [PseudoEMetricSpace M] [IsometricSMul M M] (a : M) (b : M) (c : M) :
      edist (a * b) (a * c) = edist b c
      theorem isometry_add_right {M : Type u} [Add M] [PseudoEMetricSpace M] [IsometricVAdd Mᵃᵒᵖ M] (a : M) :
      Isometry fun x => x + a
      theorem isometry_mul_right {M : Type u} [Mul M] [PseudoEMetricSpace M] [IsometricSMul Mᵐᵒᵖ M] (a : M) :
      Isometry fun x => x * a
      @[simp]
      theorem edist_add_right {M : Type u} [Add M] [PseudoEMetricSpace M] [IsometricVAdd Mᵃᵒᵖ M] (a : M) (b : M) (c : M) :
      edist (a + c) (b + c) = edist a b
      @[simp]
      theorem edist_mul_right {M : Type u} [Mul M] [PseudoEMetricSpace M] [IsometricSMul Mᵐᵒᵖ M] (a : M) (b : M) (c : M) :
      edist (a * c) (b * c) = edist a b
      @[simp]
      theorem edist_sub_right {M : Type u} [SubNegMonoid M] [PseudoEMetricSpace M] [IsometricVAdd Mᵃᵒᵖ M] (a : M) (b : M) (c : M) :
      edist (a - c) (b - c) = edist a b
      @[simp]
      theorem edist_div_right {M : Type u} [DivInvMonoid M] [PseudoEMetricSpace M] [IsometricSMul Mᵐᵒᵖ M] (a : M) (b : M) (c : M) :
      edist (a / c) (b / c) = edist a b
      @[simp]
      theorem edist_neg_neg {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd G G] [IsometricVAdd Gᵃᵒᵖ G] (a : G) (b : G) :
      edist (-a) (-b) = edist a b
      @[simp]
      theorem edist_inv_inv {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G] (a : G) (b : G) :
      theorem edist_neg {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd G G] [IsometricVAdd Gᵃᵒᵖ G] (x : G) (y : G) :
      edist (-x) y = edist x (-y)
      theorem edist_inv {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G] (x : G) (y : G) :
      @[simp]
      theorem edist_sub_left {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd G G] [IsometricVAdd Gᵃᵒᵖ G] (a : G) (b : G) (c : G) :
      edist (a - b) (a - c) = edist b c
      @[simp]
      theorem edist_div_left {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G] (a : G) (b : G) (c : G) :
      edist (a / b) (a / c) = edist b c
      theorem IsometryEquiv.constVAdd.proof_1 {G : Type u_2} {X : Type u_1} [PseudoEMetricSpace X] [AddGroup G] [AddAction G X] [IsometricVAdd G X] (c : G) :
      Isometry fun x => c +ᵥ x
      def IsometryEquiv.constVAdd {G : Type v} {X : Type w} [PseudoEMetricSpace X] [AddGroup G] [AddAction G X] [IsometricVAdd G X] (c : G) :
      X ≃ᵢ X

      If an additive group G acts on X by isometries, then IsometryEquiv.constVAdd is the isometry of X given by addition of a constant element of the group.

      Equations
      Instances For
        @[simp]
        theorem IsometryEquiv.constVAdd_apply {G : Type v} {X : Type w} [PseudoEMetricSpace X] [AddGroup G] [AddAction G X] [IsometricVAdd G X] (c : G) (x : X) :
        @[simp]
        theorem IsometryEquiv.constSMul_apply {G : Type v} {X : Type w} [PseudoEMetricSpace X] [Group G] [MulAction G X] [IsometricSMul G X] (c : G) (x : X) :
        def IsometryEquiv.constSMul {G : Type v} {X : Type w} [PseudoEMetricSpace X] [Group G] [MulAction G X] [IsometricSMul G X] (c : G) :
        X ≃ᵢ X

        If a group G acts on X by isometries, then IsometryEquiv.constSMul is the isometry of X given by multiplication of a constant element of the group.

        Equations
        Instances For

          Addition y ↦ x + y as an IsometryEquiv.

          Equations
          Instances For
            theorem IsometryEquiv.addLeft.proof_1 {G : Type u_1} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd G G] (c : G) (b : G) (c : G) :
            edist (c + b) (c + c) = edist b c
            @[simp]
            theorem IsometryEquiv.addLeft_apply {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd G G] (c : G) (x : G) :
            @[simp]
            theorem IsometryEquiv.mulLeft_apply {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] (c : G) (x : G) :

            Multiplication y ↦ x * y as an IsometryEquiv.

            Equations
            Instances For
              theorem IsometryEquiv.addRight.proof_1 {G : Type u_1} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd Gᵃᵒᵖ G] (c : G) (a : G) (b : G) :
              edist (a + c) (b + c) = edist a b

              Addition y ↦ y + x as an IsometryEquiv.

              Equations
              Instances For
                @[simp]
                @[simp]

                Multiplication y ↦ y * x as an IsometryEquiv.

                Equations
                Instances For

                  Subtraction y ↦ y - x as an IsometryEquiv.

                  Equations
                  Instances For
                    theorem IsometryEquiv.subRight.proof_1 {G : Type u_1} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd Gᵃᵒᵖ G] (c : G) (a : G) (b : G) :
                    edist (a - c) (b - c) = edist a b
                    @[simp]
                    @[simp]

                    Division y ↦ y / x as an IsometryEquiv.

                    Equations
                    Instances For

                      Subtraction y ↦ x - y as an IsometryEquiv.

                      Equations
                      Instances For
                        @[simp]
                        @[simp]

                        Division y ↦ x / y as an IsometryEquiv.

                        Equations
                        Instances For

                          Negation x ↦ -x as an IsometryEquiv.

                          Equations
                          Instances For
                            @[simp]
                            @[simp]

                            Inversion x ↦ x⁻¹ as an IsometryEquiv.

                            Equations
                            Instances For
                              @[simp]
                              theorem EMetric.vadd_ball {G : Type v} {X : Type w} [PseudoEMetricSpace X] [AddGroup G] [AddAction G X] [IsometricVAdd G X] (c : G) (x : X) (r : ENNReal) :
                              @[simp]
                              theorem EMetric.smul_ball {G : Type v} {X : Type w} [PseudoEMetricSpace X] [Group G] [MulAction G X] [IsometricSMul G X] (c : G) (x : X) (r : ENNReal) :
                              @[simp]
                              theorem EMetric.preimage_vadd_ball {G : Type v} {X : Type w} [PseudoEMetricSpace X] [AddGroup G] [AddAction G X] [IsometricVAdd G X] (c : G) (x : X) (r : ENNReal) :
                              (fun x x_1 => x +ᵥ x_1) c ⁻¹' EMetric.ball x r = EMetric.ball (-c +ᵥ x) r
                              @[simp]
                              theorem EMetric.preimage_smul_ball {G : Type v} {X : Type w} [PseudoEMetricSpace X] [Group G] [MulAction G X] [IsometricSMul G X] (c : G) (x : X) (r : ENNReal) :
                              (fun x x_1 => x x_1) c ⁻¹' EMetric.ball x r = EMetric.ball (c⁻¹ x) r
                              @[simp]
                              theorem EMetric.vadd_closedBall {G : Type v} {X : Type w} [PseudoEMetricSpace X] [AddGroup G] [AddAction G X] [IsometricVAdd G X] (c : G) (x : X) (r : ENNReal) :
                              @[simp]
                              theorem EMetric.smul_closedBall {G : Type v} {X : Type w} [PseudoEMetricSpace X] [Group G] [MulAction G X] [IsometricSMul G X] (c : G) (x : X) (r : ENNReal) :
                              @[simp]
                              theorem EMetric.preimage_vadd_closedBall {G : Type v} {X : Type w} [PseudoEMetricSpace X] [AddGroup G] [AddAction G X] [IsometricVAdd G X] (c : G) (x : X) (r : ENNReal) :
                              (fun x x_1 => x +ᵥ x_1) c ⁻¹' EMetric.closedBall x r = EMetric.closedBall (-c +ᵥ x) r
                              @[simp]
                              theorem EMetric.preimage_smul_closedBall {G : Type v} {X : Type w} [PseudoEMetricSpace X] [Group G] [MulAction G X] [IsometricSMul G X] (c : G) (x : X) (r : ENNReal) :
                              (fun x x_1 => x x_1) c ⁻¹' EMetric.closedBall x r = EMetric.closedBall (c⁻¹ x) r
                              @[simp]
                              theorem EMetric.preimage_add_left_ball {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd G G] (a : G) (b : G) (r : ENNReal) :
                              (fun x x_1 => x + x_1) a ⁻¹' EMetric.ball b r = EMetric.ball (-a + b) r
                              @[simp]
                              theorem EMetric.preimage_mul_left_ball {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] (a : G) (b : G) (r : ENNReal) :
                              (fun x x_1 => x * x_1) a ⁻¹' EMetric.ball b r = EMetric.ball (a⁻¹ * b) r
                              @[simp]
                              theorem EMetric.preimage_add_right_ball {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd Gᵃᵒᵖ G] (a : G) (b : G) (r : ENNReal) :
                              (fun x => x + a) ⁻¹' EMetric.ball b r = EMetric.ball (b - a) r
                              @[simp]
                              theorem EMetric.preimage_mul_right_ball {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul Gᵐᵒᵖ G] (a : G) (b : G) (r : ENNReal) :
                              (fun x => x * a) ⁻¹' EMetric.ball b r = EMetric.ball (b / a) r
                              @[simp]
                              theorem EMetric.preimage_add_left_closedBall {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd G G] (a : G) (b : G) (r : ENNReal) :
                              (fun x x_1 => x + x_1) a ⁻¹' EMetric.closedBall b r = EMetric.closedBall (-a + b) r
                              @[simp]
                              theorem EMetric.preimage_mul_left_closedBall {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] (a : G) (b : G) (r : ENNReal) :
                              (fun x x_1 => x * x_1) a ⁻¹' EMetric.closedBall b r = EMetric.closedBall (a⁻¹ * b) r
                              @[simp]
                              @[simp]
                              @[simp]
                              theorem dist_vadd {M : Type u} {X : Type w} [PseudoMetricSpace X] [VAdd M X] [IsometricVAdd M X] (c : M) (x : X) (y : X) :
                              dist (c +ᵥ x) (c +ᵥ y) = dist x y
                              @[simp]
                              theorem dist_smul {M : Type u} {X : Type w} [PseudoMetricSpace X] [SMul M X] [IsometricSMul M X] (c : M) (x : X) (y : X) :
                              dist (c x) (c y) = dist x y
                              @[simp]
                              theorem nndist_vadd {M : Type u} {X : Type w} [PseudoMetricSpace X] [VAdd M X] [IsometricVAdd M X] (c : M) (x : X) (y : X) :
                              nndist (c +ᵥ x) (c +ᵥ y) = nndist x y
                              @[simp]
                              theorem nndist_smul {M : Type u} {X : Type w} [PseudoMetricSpace X] [SMul M X] [IsometricSMul M X] (c : M) (x : X) (y : X) :
                              nndist (c x) (c y) = nndist x y
                              @[simp]
                              theorem diam_vadd {M : Type u} {X : Type w} [PseudoMetricSpace X] [VAdd M X] [IsometricVAdd M X] (c : M) (s : Set X) :
                              @[simp]
                              theorem diam_smul {M : Type u} {X : Type w} [PseudoMetricSpace X] [SMul M X] [IsometricSMul M X] (c : M) (s : Set X) :
                              @[simp]
                              theorem dist_add_left {M : Type u} [PseudoMetricSpace M] [Add M] [IsometricVAdd M M] (a : M) (b : M) (c : M) :
                              dist (a + b) (a + c) = dist b c
                              @[simp]
                              theorem dist_mul_left {M : Type u} [PseudoMetricSpace M] [Mul M] [IsometricSMul M M] (a : M) (b : M) (c : M) :
                              dist (a * b) (a * c) = dist b c
                              @[simp]
                              theorem nndist_add_left {M : Type u} [PseudoMetricSpace M] [Add M] [IsometricVAdd M M] (a : M) (b : M) (c : M) :
                              nndist (a + b) (a + c) = nndist b c
                              @[simp]
                              theorem nndist_mul_left {M : Type u} [PseudoMetricSpace M] [Mul M] [IsometricSMul M M] (a : M) (b : M) (c : M) :
                              nndist (a * b) (a * c) = nndist b c
                              @[simp]
                              theorem dist_add_right {M : Type u} [Add M] [PseudoMetricSpace M] [IsometricVAdd Mᵃᵒᵖ M] (a : M) (b : M) (c : M) :
                              dist (a + c) (b + c) = dist a b
                              @[simp]
                              theorem dist_mul_right {M : Type u} [Mul M] [PseudoMetricSpace M] [IsometricSMul Mᵐᵒᵖ M] (a : M) (b : M) (c : M) :
                              dist (a * c) (b * c) = dist a b
                              @[simp]
                              theorem nndist_add_right {M : Type u} [PseudoMetricSpace M] [Add M] [IsometricVAdd Mᵃᵒᵖ M] (a : M) (b : M) (c : M) :
                              nndist (a + c) (b + c) = nndist a b
                              @[simp]
                              theorem nndist_mul_right {M : Type u} [PseudoMetricSpace M] [Mul M] [IsometricSMul Mᵐᵒᵖ M] (a : M) (b : M) (c : M) :
                              nndist (a * c) (b * c) = nndist a b
                              @[simp]
                              theorem dist_sub_right {M : Type u} [SubNegMonoid M] [PseudoMetricSpace M] [IsometricVAdd Mᵃᵒᵖ M] (a : M) (b : M) (c : M) :
                              dist (a - c) (b - c) = dist a b
                              @[simp]
                              theorem dist_div_right {M : Type u} [DivInvMonoid M] [PseudoMetricSpace M] [IsometricSMul Mᵐᵒᵖ M] (a : M) (b : M) (c : M) :
                              dist (a / c) (b / c) = dist a b
                              @[simp]
                              theorem nndist_sub_right {M : Type u} [SubNegMonoid M] [PseudoMetricSpace M] [IsometricVAdd Mᵃᵒᵖ M] (a : M) (b : M) (c : M) :
                              nndist (a - c) (b - c) = nndist a b
                              @[simp]
                              theorem nndist_div_right {M : Type u} [DivInvMonoid M] [PseudoMetricSpace M] [IsometricSMul Mᵐᵒᵖ M] (a : M) (b : M) (c : M) :
                              nndist (a / c) (b / c) = nndist a b
                              @[simp]
                              theorem dist_neg_neg {G : Type v} [AddGroup G] [PseudoMetricSpace G] [IsometricVAdd G G] [IsometricVAdd Gᵃᵒᵖ G] (a : G) (b : G) :
                              dist (-a) (-b) = dist a b
                              @[simp]
                              theorem dist_inv_inv {G : Type v} [Group G] [PseudoMetricSpace G] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G] (a : G) (b : G) :
                              @[simp]
                              theorem nndist_neg_neg {G : Type v} [AddGroup G] [PseudoMetricSpace G] [IsometricVAdd G G] [IsometricVAdd Gᵃᵒᵖ G] (a : G) (b : G) :
                              nndist (-a) (-b) = nndist a b
                              @[simp]
                              theorem nndist_inv_inv {G : Type v} [Group G] [PseudoMetricSpace G] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G] (a : G) (b : G) :
                              @[simp]
                              theorem dist_sub_left {G : Type v} [AddGroup G] [PseudoMetricSpace G] [IsometricVAdd G G] [IsometricVAdd Gᵃᵒᵖ G] (a : G) (b : G) (c : G) :
                              dist (a - b) (a - c) = dist b c
                              @[simp]
                              theorem dist_div_left {G : Type v} [Group G] [PseudoMetricSpace G] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G] (a : G) (b : G) (c : G) :
                              dist (a / b) (a / c) = dist b c
                              @[simp]
                              theorem nndist_sub_left {G : Type v} [AddGroup G] [PseudoMetricSpace G] [IsometricVAdd G G] [IsometricVAdd Gᵃᵒᵖ G] (a : G) (b : G) (c : G) :
                              nndist (a - b) (a - c) = nndist b c
                              @[simp]
                              theorem nndist_div_left {G : Type v} [Group G] [PseudoMetricSpace G] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G] (a : G) (b : G) (c : G) :
                              nndist (a / b) (a / c) = nndist b c
                              theorem Bornology.IsBounded.vadd {G : Type v} {X : Type w} [PseudoMetricSpace X] [VAdd G X] [IsometricVAdd G X] {s : Set X} (hs : Bornology.IsBounded s) (c : G) :

                              Given an additive isometric action of G on X, the image of a bounded set in X under translation by c : G is bounded

                              theorem Bornology.IsBounded.smul {G : Type v} {X : Type w} [PseudoMetricSpace X] [SMul G X] [IsometricSMul G X] {s : Set X} (hs : Bornology.IsBounded s) (c : G) :

                              If G acts isometrically on X, then the image of a bounded set in X under scalar multiplication by c : G is bounded. See also Bornology.IsBounded.smul₀ for a similar lemma about normed spaces.

                              @[simp]
                              theorem Metric.vadd_ball {G : Type v} {X : Type w} [PseudoMetricSpace X] [AddGroup G] [AddAction G X] [IsometricVAdd G X] (c : G) (x : X) (r : ) :
                              @[simp]
                              theorem Metric.smul_ball {G : Type v} {X : Type w} [PseudoMetricSpace X] [Group G] [MulAction G X] [IsometricSMul G X] (c : G) (x : X) (r : ) :
                              @[simp]
                              theorem Metric.preimage_vadd_ball {G : Type v} {X : Type w} [PseudoMetricSpace X] [AddGroup G] [AddAction G X] [IsometricVAdd G X] (c : G) (x : X) (r : ) :
                              (fun x x_1 => x +ᵥ x_1) c ⁻¹' Metric.ball x r = Metric.ball (-c +ᵥ x) r
                              @[simp]
                              theorem Metric.preimage_smul_ball {G : Type v} {X : Type w} [PseudoMetricSpace X] [Group G] [MulAction G X] [IsometricSMul G X] (c : G) (x : X) (r : ) :
                              (fun x x_1 => x x_1) c ⁻¹' Metric.ball x r = Metric.ball (c⁻¹ x) r
                              @[simp]
                              theorem Metric.vadd_closedBall {G : Type v} {X : Type w} [PseudoMetricSpace X] [AddGroup G] [AddAction G X] [IsometricVAdd G X] (c : G) (x : X) (r : ) :
                              @[simp]
                              theorem Metric.smul_closedBall {G : Type v} {X : Type w} [PseudoMetricSpace X] [Group G] [MulAction G X] [IsometricSMul G X] (c : G) (x : X) (r : ) :
                              @[simp]
                              theorem Metric.preimage_vadd_closedBall {G : Type v} {X : Type w} [PseudoMetricSpace X] [AddGroup G] [AddAction G X] [IsometricVAdd G X] (c : G) (x : X) (r : ) :
                              (fun x x_1 => x +ᵥ x_1) c ⁻¹' Metric.closedBall x r = Metric.closedBall (-c +ᵥ x) r
                              @[simp]
                              theorem Metric.preimage_smul_closedBall {G : Type v} {X : Type w} [PseudoMetricSpace X] [Group G] [MulAction G X] [IsometricSMul G X] (c : G) (x : X) (r : ) :
                              (fun x x_1 => x x_1) c ⁻¹' Metric.closedBall x r = Metric.closedBall (c⁻¹ x) r
                              @[simp]
                              theorem Metric.vadd_sphere {G : Type v} {X : Type w} [PseudoMetricSpace X] [AddGroup G] [AddAction G X] [IsometricVAdd G X] (c : G) (x : X) (r : ) :
                              @[simp]
                              theorem Metric.smul_sphere {G : Type v} {X : Type w} [PseudoMetricSpace X] [Group G] [MulAction G X] [IsometricSMul G X] (c : G) (x : X) (r : ) :
                              @[simp]
                              theorem Metric.preimage_vadd_sphere {G : Type v} {X : Type w} [PseudoMetricSpace X] [AddGroup G] [AddAction G X] [IsometricVAdd G X] (c : G) (x : X) (r : ) :
                              (fun x x_1 => x +ᵥ x_1) c ⁻¹' Metric.sphere x r = Metric.sphere (-c +ᵥ x) r
                              @[simp]
                              theorem Metric.preimage_smul_sphere {G : Type v} {X : Type w} [PseudoMetricSpace X] [Group G] [MulAction G X] [IsometricSMul G X] (c : G) (x : X) (r : ) :
                              (fun x x_1 => x x_1) c ⁻¹' Metric.sphere x r = Metric.sphere (c⁻¹ x) r
                              @[simp]
                              theorem Metric.preimage_add_left_ball {G : Type v} [AddGroup G] [PseudoMetricSpace G] [IsometricVAdd G G] (a : G) (b : G) (r : ) :
                              (fun x x_1 => x + x_1) a ⁻¹' Metric.ball b r = Metric.ball (-a + b) r
                              @[simp]
                              theorem Metric.preimage_mul_left_ball {G : Type v} [Group G] [PseudoMetricSpace G] [IsometricSMul G G] (a : G) (b : G) (r : ) :
                              (fun x x_1 => x * x_1) a ⁻¹' Metric.ball b r = Metric.ball (a⁻¹ * b) r
                              @[simp]
                              theorem Metric.preimage_add_right_ball {G : Type v} [AddGroup G] [PseudoMetricSpace G] [IsometricVAdd Gᵃᵒᵖ G] (a : G) (b : G) (r : ) :
                              (fun x => x + a) ⁻¹' Metric.ball b r = Metric.ball (b - a) r
                              @[simp]
                              theorem Metric.preimage_mul_right_ball {G : Type v} [Group G] [PseudoMetricSpace G] [IsometricSMul Gᵐᵒᵖ G] (a : G) (b : G) (r : ) :
                              (fun x => x * a) ⁻¹' Metric.ball b r = Metric.ball (b / a) r
                              @[simp]
                              theorem Metric.preimage_add_left_closedBall {G : Type v} [AddGroup G] [PseudoMetricSpace G] [IsometricVAdd G G] (a : G) (b : G) (r : ) :
                              (fun x x_1 => x + x_1) a ⁻¹' Metric.closedBall b r = Metric.closedBall (-a + b) r
                              @[simp]
                              theorem Metric.preimage_mul_left_closedBall {G : Type v} [Group G] [PseudoMetricSpace G] [IsometricSMul G G] (a : G) (b : G) (r : ) :
                              (fun x x_1 => x * x_1) a ⁻¹' Metric.closedBall b r = Metric.closedBall (a⁻¹ * b) r
                              @[simp]
                              theorem Metric.preimage_add_right_closedBall {G : Type v} [AddGroup G] [PseudoMetricSpace G] [IsometricVAdd Gᵃᵒᵖ G] (a : G) (b : G) (r : ) :
                              (fun x => x + a) ⁻¹' Metric.closedBall b r = Metric.closedBall (b - a) r
                              @[simp]
                              theorem Metric.preimage_mul_right_closedBall {G : Type v} [Group G] [PseudoMetricSpace G] [IsometricSMul Gᵐᵒᵖ G] (a : G) (b : G) (r : ) :
                              (fun x => x * a) ⁻¹' Metric.closedBall b r = Metric.closedBall (b / a) r
                              theorem instIsometricVAddForAllPseudoEMetricSpacePiInstVAdd.proof_1 {M : Type u_1} {ι : Type u_2} {X : ιType u_3} [Fintype ι] [(i : ι) → VAdd M (X i)] [(i : ι) → PseudoEMetricSpace (X i)] [∀ (i : ι), IsometricVAdd M (X i)] :
                              IsometricVAdd M ((i : ι) → X i)
                              instance instIsometricVAddForAllPseudoEMetricSpacePiInstVAdd {M : Type u} {ι : Type u_3} {X : ιType u_2} [Fintype ι] [(i : ι) → VAdd M (X i)] [(i : ι) → PseudoEMetricSpace (X i)] [∀ (i : ι), IsometricVAdd M (X i)] :
                              IsometricVAdd M ((i : ι) → X i)
                              Equations
                              instance instIsometricSMulForAllPseudoEMetricSpacePiInstSMul {M : Type u} {ι : Type u_3} {X : ιType u_2} [Fintype ι] [(i : ι) → SMul M (X i)] [(i : ι) → PseudoEMetricSpace (X i)] [∀ (i : ι), IsometricSMul M (X i)] :
                              IsometricSMul M ((i : ι) → X i)
                              Equations
                              instance Pi.isometricVAdd' {ι : Type u_4} {M : ιType u_2} {X : ιType u_3} [Fintype ι] [(i : ι) → VAdd (M i) (X i)] [(i : ι) → PseudoEMetricSpace (X i)] [∀ (i : ι), IsometricVAdd (M i) (X i)] :
                              IsometricVAdd ((i : ι) → M i) ((i : ι) → X i)
                              Equations
                              theorem Pi.isometricVAdd'.proof_1 {ι : Type u_1} {M : ιType u_2} {X : ιType u_3} [Fintype ι] [(i : ι) → VAdd (M i) (X i)] [(i : ι) → PseudoEMetricSpace (X i)] [∀ (i : ι), IsometricVAdd (M i) (X i)] :
                              IsometricVAdd ((i : ι) → M i) ((i : ι) → X i)
                              instance Pi.isometricSMul' {ι : Type u_4} {M : ιType u_2} {X : ιType u_3} [Fintype ι] [(i : ι) → SMul (M i) (X i)] [(i : ι) → PseudoEMetricSpace (X i)] [∀ (i : ι), IsometricSMul (M i) (X i)] :
                              IsometricSMul ((i : ι) → M i) ((i : ι) → X i)
                              Equations
                              instance Pi.isometricVAdd'' {ι : Type u_3} {M : ιType u_2} [Fintype ι] [(i : ι) → Add (M i)] [(i : ι) → PseudoEMetricSpace (M i)] [∀ (i : ι), IsometricVAdd (M i)ᵃᵒᵖ (M i)] :
                              IsometricVAdd ((i : ι) → M i)ᵃᵒᵖ ((i : ι) → M i)
                              Equations
                              theorem Pi.isometricVAdd''.proof_1 {ι : Type u_1} {M : ιType u_2} [Fintype ι] [(i : ι) → Add (M i)] [(i : ι) → PseudoEMetricSpace (M i)] [∀ (i : ι), IsometricVAdd (M i)ᵃᵒᵖ (M i)] :
                              IsometricVAdd ((i : ι) → M i)ᵃᵒᵖ ((i : ι) → M i)
                              instance Pi.isometricSMul'' {ι : Type u_3} {M : ιType u_2} [Fintype ι] [(i : ι) → Mul (M i)] [(i : ι) → PseudoEMetricSpace (M i)] [∀ (i : ι), IsometricSMul (M i)ᵐᵒᵖ (M i)] :
                              IsometricSMul ((i : ι) → M i)ᵐᵒᵖ ((i : ι) → M i)
                              Equations