Group actions by isometries

In this file we define two typeclasses:

• IsometricSMul M X says that M multiplicatively acts on a (pseudo extended) metric space X by isometries;
• IsometricVAdd is an additive version of IsometricSMul.

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] : Prop

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

• isometry_vadd : ∀ (c : M), Isometry fun (x : X) => c +ᵥ x

Instances

• AddUnits.isometricVAdd
• Additive.isometricVAdd
• Additive.isometricVAdd'
• Additive.isometricVAdd''
• IsometricVAdd.opposite_of_comm
• NormedAddGroup.to_isometricVAdd_left
• NormedAddGroup.to_isometricVAdd_right
• NormedAddTorsor.to_isometricVAdd
• Pi.isometricVAdd'
• Pi.isometricVAdd''
• Prod.isometricVAdd'
• Prod.isometricVAdd''
• ULift.isometricVAdd
• ULift.isometricVAdd'
• instIsometricVAddAddOppositeInstPseudoEMetricSpaceAddOppositeVadd
• instIsometricVAddForAllPseudoEMetricSpacePiInstVAdd
• instIsometricVAddSumPseudoEMetricSpaceMaxVadd

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

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

• isometry_smul : ∀ (c : M), Isometry fun (x : X) => c • x

Instances

• DomMulAct.instIsometricSMulDomMulActSubtypeAEEqFunToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupMemAddSubgroupInstAddGroupToAddGroupToNormedAddGroupToTopologicalAddGroupInstMembershipInstSetLikeAddSubgroupLpToPseudoEMetricSpaceToEMetricSpaceToMetricSpaceInstNormedAddCommGroupInstSMulDomMulActSubtypeAEEqFunToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupMemAddSubgroupInstAddGroupToAddGroupToNormedAddGroupToTopologicalAddGroupInstMembershipInstSetLikeAddSubgroupLp
• IsometricSMul.opposite_of_comm
• Multiplicative.isometricSMul
• Multiplicative.isometricSMul'
• Multiplicative.isometricVAdd''
• NormedGroup.to_isometricSMul_left
• NormedGroup.to_isometricSMul_right
• Pi.isometricSMul'
• Pi.isometricSMul''
• Prod.isometricSMul'
• Prod.isometricSMul''
• ULift.isometricSMul
• ULift.isometricSMul'
• Units.isometricSMul
• UpperHalfPlane.instIsometricSMulSpecialLinearGroupFinOfNatNatInstOfNatNatInstDecidableEqFinFintypeRealCommRingUpperHalfPlaneToPseudoEMetricSpaceToEMetricSpaceInstMetricSpaceUpperHalfPlaneToSMulMonoidSLActionToAlgebraNormedFieldToSeminormedRingToSeminormedCommRingNormedCommRingToNormedAlgebraIsROrC
• instIsometricSMulForAllPseudoEMetricSpacePiInstSMul
• instIsometricSMulMulOppositeInstPseudoEMetricSpaceMulOppositeSmul
• instIsometricSMulProdPseudoEMetricSpaceMaxSmul

theorem isometry_vadd {M : Type u} (X : Type w) [PseudoEMetricSpace X] [VAdd M X] [IsometricVAdd M X] (c : M) : Isometry fun (x : 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 : X) => c • x

instance IsometricVAdd.to_continuousConstVAdd (M : Type u) (X : Type w) [PseudoEMetricSpace X] [VAdd M X] [IsometricVAdd M X] : ContinuousConstVAdd M X

Equations

• (_ : ContinuousConstVAdd M X) = (_ : ContinuousConstVAdd M X)

instance IsometricSMul.to_continuousConstSMul (M : Type u) (X : Type w) [PseudoEMetricSpace X] [SMul M X] [IsometricSMul M X] : ContinuousConstSMul M X

Equations

• (_ : ContinuousConstSMul M X) = (_ : ContinuousConstSMul M X)

instance IsometricVAdd.opposite_of_comm (M : Type u) (X : Type w) [PseudoEMetricSpace X] [VAdd M X] [VAdd Mᵃᵒᵖ X] [IsCentralVAdd M X] [IsometricVAdd M X] : IsometricVAdd Mᵃᵒᵖ X

Equations

• (_ : IsometricVAdd Mᵃᵒᵖ X) = (_ : IsometricVAdd Mᵃᵒᵖ X)

instance IsometricSMul.opposite_of_comm (M : Type u) (X : Type w) [PseudoEMetricSpace X] [SMul M X] [SMul Mᵐᵒᵖ X] [IsCentralScalar M X] [IsometricSMul M X] : IsometricSMul Mᵐᵒᵖ X

Equations

• (_ : IsometricSMul Mᵐᵒᵖ X) = (_ : IsometricSMul Mᵐᵒᵖ 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) : EMetric.diam (c +ᵥ s) = EMetric.diam s

@[simp]

theorem ediam_smul {M : Type u} {X : Type w} [PseudoEMetricSpace X] [SMul M X] [IsometricSMul M X] (c : M) (s : Set X) : EMetric.diam (c • s) = EMetric.diam s

theorem isometry_add_left {M : Type u} [Add M] [PseudoEMetricSpace M] [IsometricVAdd M M] (a : M) : Isometry fun (x : M) => a + x

theorem isometry_mul_left {M : Type u} [Mul M] [PseudoEMetricSpace M] [IsometricSMul M M] (a : M) : Isometry fun (x : M) => a * x

@[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 : M) => x + a

theorem isometry_mul_right {M : Type u} [Mul M] [PseudoEMetricSpace M] [IsometricSMul Mᵐᵒᵖ M] (a : M) : Isometry fun (x : M) => 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) : edist a⁻¹ b⁻¹ = edist a b

theorem isometry_neg {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd G G] [IsometricVAdd Gᵃᵒᵖ G] : Isometry Neg.neg

theorem isometry_inv {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G] : Isometry Inv.inv

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) : edist x⁻¹ y = edist x y⁻¹

@[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 : 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

• IsometryEquiv.constVAdd c = { toEquiv := AddAction.toPerm c, isometry_toFun := (_ : Isometry fun (x : X) => c +ᵥ x) }

@[simp]

theorem IsometryEquiv.constSMul_toEquiv {G : Type v} {X : Type w} [PseudoEMetricSpace X] [Group G] [MulAction G X] [IsometricSMul G X] (c : G) : (IsometryEquiv.constSMul c).toEquiv = MulAction.toPerm c

@[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) : (IsometryEquiv.constSMul c) x = c • x

@[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) : (IsometryEquiv.constVAdd c) x = c +ᵥ x

@[simp]

theorem IsometryEquiv.constVAdd_toEquiv {G : Type v} {X : Type w} [PseudoEMetricSpace X] [AddGroup G] [AddAction G X] [IsometricVAdd G X] (c : G) : (IsometryEquiv.constVAdd c).toEquiv = AddAction.toPerm c

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

• IsometryEquiv.constSMul c = { toEquiv := MulAction.toPerm c, isometry_toFun := (_ : Isometry fun (x : X) => c • x) }

@[simp]

theorem IsometryEquiv.constVAdd_symm {G : Type v} {X : Type w} [PseudoEMetricSpace X] [AddGroup G] [AddAction G X] [IsometricVAdd G X] (c : G) : IsometryEquiv.symm (IsometryEquiv.constVAdd c) = IsometryEquiv.constVAdd (-c)

@[simp]

theorem IsometryEquiv.constSMul_symm {G : Type v} {X : Type w} [PseudoEMetricSpace X] [Group G] [MulAction G X] [IsometricSMul G X] (c : G) : IsometryEquiv.symm (IsometryEquiv.constSMul c) = IsometryEquiv.constSMul c⁻¹

def IsometryEquiv.addLeft {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd G G] (c : G) : G ≃ᵢ G

Addition y ↦ x + y as an IsometryEquiv.

Equations

• IsometryEquiv.addLeft c = { toEquiv := Equiv.addLeft c, isometry_toFun := (_ : ∀ (b c_1 : G), edist (c + b) (c + c_1) = edist b c_1) }

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.mulLeft_apply {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] (c : G) (x : G) : (IsometryEquiv.mulLeft c) x = c * x

@[simp]

theorem IsometryEquiv.addLeft_apply {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd G G] (c : G) (x : G) : (IsometryEquiv.addLeft c) x = c + x

@[simp]

theorem IsometryEquiv.addLeft_toEquiv {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd G G] (c : G) : (IsometryEquiv.addLeft c).toEquiv = Equiv.addLeft c

@[simp]

theorem IsometryEquiv.mulLeft_toEquiv {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] (c : G) : (IsometryEquiv.mulLeft c).toEquiv = Equiv.mulLeft c

def IsometryEquiv.mulLeft {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] (c : G) : G ≃ᵢ G

Multiplication y ↦ x * y as an IsometryEquiv.

Equations

• IsometryEquiv.mulLeft c = { toEquiv := Equiv.mulLeft c, isometry_toFun := (_ : ∀ (b c_1 : G), edist (c * b) (c * c_1) = edist b c_1) }

@[simp]

theorem IsometryEquiv.addLeft_symm {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd G G] (x : G) : IsometryEquiv.symm (IsometryEquiv.addLeft x) = IsometryEquiv.addLeft (-x)

@[simp]

theorem IsometryEquiv.mulLeft_symm {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] (x : G) : IsometryEquiv.symm (IsometryEquiv.mulLeft x) = IsometryEquiv.mulLeft x⁻¹

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

def IsometryEquiv.addRight {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd Gᵃᵒᵖ G] (c : G) : G ≃ᵢ G

Addition y ↦ y + x as an IsometryEquiv.

Equations

• IsometryEquiv.addRight c = { toEquiv := Equiv.addRight c, isometry_toFun := (_ : ∀ (a b : G), edist (a + c) (b + c) = edist a b) }

@[simp]

theorem IsometryEquiv.mulRight_apply {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul Gᵐᵒᵖ G] (c : G) (x : G) : (IsometryEquiv.mulRight c) x = x * c

@[simp]

theorem IsometryEquiv.addRight_toEquiv {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd Gᵃᵒᵖ G] (c : G) : (IsometryEquiv.addRight c).toEquiv = Equiv.addRight c

@[simp]

theorem IsometryEquiv.mulRight_toEquiv {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul Gᵐᵒᵖ G] (c : G) : (IsometryEquiv.mulRight c).toEquiv = Equiv.mulRight c

@[simp]

theorem IsometryEquiv.addRight_apply {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd Gᵃᵒᵖ G] (c : G) (x : G) : (IsometryEquiv.addRight c) x = x + c

def IsometryEquiv.mulRight {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul Gᵐᵒᵖ G] (c : G) : G ≃ᵢ G

Multiplication y ↦ y * x as an IsometryEquiv.

Equations

• IsometryEquiv.mulRight c = { toEquiv := Equiv.mulRight c, isometry_toFun := (_ : ∀ (a b : G), edist (a * c) (b * c) = edist a b) }

@[simp]

theorem IsometryEquiv.addRight_symm {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd Gᵃᵒᵖ G] (x : G) : IsometryEquiv.symm (IsometryEquiv.addRight x) = IsometryEquiv.addRight (-x)

@[simp]

theorem IsometryEquiv.mulRight_symm {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul Gᵐᵒᵖ G] (x : G) : IsometryEquiv.symm (IsometryEquiv.mulRight x) = IsometryEquiv.mulRight x⁻¹

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

def IsometryEquiv.subRight {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd Gᵃᵒᵖ G] (c : G) : G ≃ᵢ G

Subtraction y ↦ y - x as an IsometryEquiv.

Equations

• IsometryEquiv.subRight c = { toEquiv := Equiv.subRight c, isometry_toFun := (_ : ∀ (a b : G), edist (a - c) (b - c) = edist a b) }

@[simp]

theorem IsometryEquiv.divRight_apply {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul Gᵐᵒᵖ G] (c : G) (b : G) : (IsometryEquiv.divRight c) b = b / c

@[simp]

theorem IsometryEquiv.divRight_toEquiv {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul Gᵐᵒᵖ G] (c : G) : (IsometryEquiv.divRight c).toEquiv = Equiv.divRight c

@[simp]

theorem IsometryEquiv.subRight_toEquiv {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd Gᵃᵒᵖ G] (c : G) : (IsometryEquiv.subRight c).toEquiv = Equiv.subRight c

@[simp]

theorem IsometryEquiv.subRight_apply {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd Gᵃᵒᵖ G] (c : G) (b : G) : (IsometryEquiv.subRight c) b = b - c

def IsometryEquiv.divRight {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul Gᵐᵒᵖ G] (c : G) : G ≃ᵢ G

Division y ↦ y / x as an IsometryEquiv.

Equations

• IsometryEquiv.divRight c = { toEquiv := Equiv.divRight c, isometry_toFun := (_ : ∀ (a b : G), edist (a / c) (b / c) = edist a b) }

@[simp]

theorem IsometryEquiv.subRight_symm {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd Gᵃᵒᵖ G] (c : G) : IsometryEquiv.symm (IsometryEquiv.subRight c) = IsometryEquiv.addRight c

@[simp]

theorem IsometryEquiv.divRight_symm {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul Gᵐᵒᵖ G] (c : G) : IsometryEquiv.symm (IsometryEquiv.divRight c) = IsometryEquiv.mulRight c

def IsometryEquiv.subLeft {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd G G] [IsometricVAdd Gᵃᵒᵖ G] (c : G) : G ≃ᵢ G

Subtraction y ↦ x - y as an IsometryEquiv.

Equations

• IsometryEquiv.subLeft c = { toEquiv := Equiv.subLeft c, isometry_toFun := (_ : ∀ (b c_1 : G), edist (c - b) (c - c_1) = edist b c_1) }

@[simp]

theorem IsometryEquiv.subLeft_symm_apply {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd G G] [IsometricVAdd Gᵃᵒᵖ G] (c : G) (b : G) : (IsometryEquiv.symm (IsometryEquiv.subLeft c)) b = -b + c

@[simp]

theorem IsometryEquiv.divLeft_toEquiv {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G] (c : G) : (IsometryEquiv.divLeft c).toEquiv = Equiv.divLeft c

@[simp]

theorem IsometryEquiv.subLeft_apply {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd G G] [IsometricVAdd Gᵃᵒᵖ G] (c : G) (b : G) : (IsometryEquiv.subLeft c) b = c - b

@[simp]

theorem IsometryEquiv.subLeft_toEquiv {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd G G] [IsometricVAdd Gᵃᵒᵖ G] (c : G) : (IsometryEquiv.subLeft c).toEquiv = Equiv.subLeft c

@[simp]

theorem IsometryEquiv.divLeft_symm_apply {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G] (c : G) (b : G) : (IsometryEquiv.symm (IsometryEquiv.divLeft c)) b = b⁻¹ * c

@[simp]

theorem IsometryEquiv.divLeft_apply {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G] (c : G) (b : G) : (IsometryEquiv.divLeft c) b = c / b

def IsometryEquiv.divLeft {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G] (c : G) : G ≃ᵢ G

Division y ↦ x / y as an IsometryEquiv.

Equations

• IsometryEquiv.divLeft c = { toEquiv := Equiv.divLeft c, isometry_toFun := (_ : ∀ (b c_1 : G), edist (c / b) (c / c_1) = edist b c_1) }

def IsometryEquiv.neg (G : Type v) [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd G G] [IsometricVAdd Gᵃᵒᵖ G] : G ≃ᵢ G

Negation x ↦ -x as an IsometryEquiv.

Equations

• IsometryEquiv.neg G = { toEquiv := Equiv.neg G, isometry_toFun := (_ : ∀ (a b : G), edist (-a) (-b) = edist a b) }

@[simp]

theorem IsometryEquiv.neg_toEquiv (G : Type v) [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd G G] [IsometricVAdd Gᵃᵒᵖ G] : (IsometryEquiv.neg G).toEquiv = Equiv.neg G

@[simp]

theorem IsometryEquiv.neg_apply (G : Type v) [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd G G] [IsometricVAdd Gᵃᵒᵖ G] : ∀ (a : G), (IsometryEquiv.neg G) a = -a

@[simp]

theorem IsometryEquiv.inv_apply (G : Type v) [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G] : ∀ (a : G), (IsometryEquiv.inv G) a = a⁻¹

@[simp]

theorem IsometryEquiv.inv_toEquiv (G : Type v) [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G] : (IsometryEquiv.inv G).toEquiv = Equiv.inv G

def IsometryEquiv.inv (G : Type v) [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G] : G ≃ᵢ G

Inversion x ↦ x⁻¹ as an IsometryEquiv.

Equations

• IsometryEquiv.inv G = { toEquiv := Equiv.inv G, isometry_toFun := (_ : ∀ (a b : G), edist a⁻¹ b⁻¹ = edist a b) }

@[simp]

theorem IsometryEquiv.neg_symm (G : Type v) [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd G G] [IsometricVAdd Gᵃᵒᵖ G] : IsometryEquiv.symm (IsometryEquiv.neg G) = IsometryEquiv.neg G

@[simp]

theorem IsometryEquiv.inv_symm (G : Type v) [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G] : IsometryEquiv.symm (IsometryEquiv.inv G) = IsometryEquiv.inv G

@[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) : c +ᵥ EMetric.ball x r = EMetric.ball (c +ᵥ x) r

@[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) : c • EMetric.ball x r = EMetric.ball (c • x) r

@[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) => c +ᵥ x) ⁻¹' 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) => c • x) ⁻¹' 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) : c +ᵥ EMetric.closedBall x r = EMetric.closedBall (c +ᵥ x) r

@[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) : c • EMetric.closedBall x r = EMetric.closedBall (c • x) r

@[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) => c +ᵥ x) ⁻¹' 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) => c • x) ⁻¹' 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 : G) => a + x) ⁻¹' 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 : G) => a * x) ⁻¹' 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 : G) => 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 : G) => 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 : G) => a + x) ⁻¹' 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 : G) => a * x) ⁻¹' EMetric.closedBall b r = EMetric.closedBall (a⁻¹ * b) r

@[simp]

theorem EMetric.preimage_add_right_closedBall {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd Gᵃᵒᵖ G] (a : G) (b : G) (r : ENNReal) : (fun (x : G) => x + a) ⁻¹' EMetric.closedBall b r = EMetric.closedBall (b - a) r

@[simp]

theorem EMetric.preimage_mul_right_closedBall {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul Gᵐᵒᵖ G] (a : G) (b : G) (r : ENNReal) : (fun (x : G) => x * a) ⁻¹' EMetric.closedBall b r = EMetric.closedBall (b / a) r

@[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) : Metric.diam (c +ᵥ s) = Metric.diam s

@[simp]

theorem diam_smul {M : Type u} {X : Type w} [PseudoMetricSpace X] [SMul M X] [IsometricSMul M X] (c : M) (s : Set X) : Metric.diam (c • s) = Metric.diam s

@[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) : dist a⁻¹ b⁻¹ = dist a b

@[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) : nndist a⁻¹ b⁻¹ = nndist a b

@[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) : Bornology.IsBounded (c +ᵥ s)

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) : Bornology.IsBounded (c • s)

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 : ℝ) : c +ᵥ Metric.ball x r = Metric.ball (c +ᵥ 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 : ℝ) : c • Metric.ball x r = Metric.ball (c • 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) => c +ᵥ x) ⁻¹' 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) => c • x) ⁻¹' 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 : ℝ) : c +ᵥ Metric.closedBall x r = Metric.closedBall (c +ᵥ 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 : ℝ) : c • Metric.closedBall x r = Metric.closedBall (c • 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) => c +ᵥ x) ⁻¹' 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) => c • x) ⁻¹' 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 : ℝ) : c +ᵥ Metric.sphere x r = Metric.sphere (c +ᵥ 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 : ℝ) : c • Metric.sphere x r = Metric.sphere (c • 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) => c +ᵥ x) ⁻¹' 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) => c • x) ⁻¹' 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 : G) => a + x) ⁻¹' 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 : G) => a * x) ⁻¹' 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 : G) => 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 : G) => 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 : G) => a + x) ⁻¹' 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 : G) => a * x) ⁻¹' 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 : G) => 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 : G) => x * a) ⁻¹' Metric.closedBall b r = Metric.closedBall (b / a) r

instance instIsometricVAddSumPseudoEMetricSpaceMaxVadd {M : Type u} {X : Type w} {Y : Type u_1} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] [VAdd M X] [IsometricVAdd M X] [VAdd M Y] [IsometricVAdd M Y] : IsometricVAdd M (X × Y)

Equations

• (_ : IsometricVAdd M (X × Y)) = (_ : IsometricVAdd M (X × Y))

instance instIsometricSMulProdPseudoEMetricSpaceMaxSmul {M : Type u} {X : Type w} {Y : Type u_1} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] [SMul M X] [IsometricSMul M X] [SMul M Y] [IsometricSMul M Y] : IsometricSMul M (X × Y)

Equations

• (_ : IsometricSMul M (X × Y)) = (_ : IsometricSMul M (X × Y))

instance Prod.isometricVAdd' {M : Type u} {N : Type u_2} [Add M] [PseudoEMetricSpace M] [IsometricVAdd M M] [Add N] [PseudoEMetricSpace N] [IsometricVAdd N N] : IsometricVAdd (M × N) (M × N)

Equations

• (_ : IsometricVAdd (M × N) (M × N)) = (_ : IsometricVAdd (M × N) (M × N))

instance Prod.isometricSMul' {M : Type u} {N : Type u_2} [Mul M] [PseudoEMetricSpace M] [IsometricSMul M M] [Mul N] [PseudoEMetricSpace N] [IsometricSMul N N] : IsometricSMul (M × N) (M × N)

Equations

• (_ : IsometricSMul (M × N) (M × N)) = (_ : IsometricSMul (M × N) (M × N))

instance Prod.isometricVAdd'' {M : Type u} {N : Type u_2} [Add M] [PseudoEMetricSpace M] [IsometricVAdd Mᵃᵒᵖ M] [Add N] [PseudoEMetricSpace N] [IsometricVAdd Nᵃᵒᵖ N] : IsometricVAdd (M × N)ᵃᵒᵖ (M × N)

Equations

• (_ : IsometricVAdd (M × N)ᵃᵒᵖ (M × N)) = (_ : IsometricVAdd (M × N)ᵃᵒᵖ (M × N))

instance Prod.isometricSMul'' {M : Type u} {N : Type u_2} [Mul M] [PseudoEMetricSpace M] [IsometricSMul Mᵐᵒᵖ M] [Mul N] [PseudoEMetricSpace N] [IsometricSMul Nᵐᵒᵖ N] : IsometricSMul (M × N)ᵐᵒᵖ (M × N)

Equations

• (_ : IsometricSMul (M × N)ᵐᵒᵖ (M × N)) = (_ : IsometricSMul (M × N)ᵐᵒᵖ (M × N))

instance AddUnits.isometricVAdd {M : Type u} {X : Type w} [PseudoEMetricSpace X] [VAdd M X] [IsometricVAdd M X] [AddMonoid M] : IsometricVAdd (AddUnits M) X

Equations

• (_ : IsometricVAdd (AddUnits M) X) = (_ : IsometricVAdd (AddUnits M) X)

instance Units.isometricSMul {M : Type u} {X : Type w} [PseudoEMetricSpace X] [SMul M X] [IsometricSMul M X] [Monoid M] : IsometricSMul Mˣ X

Equations

• (_ : IsometricSMul Mˣ X) = (_ : IsometricSMul Mˣ X)

instance instIsometricVAddAddOppositeInstPseudoEMetricSpaceAddOppositeVadd {M : Type u} {X : Type w} [PseudoEMetricSpace X] [VAdd M X] [IsometricVAdd M X] : IsometricVAdd M Xᵃᵒᵖ

Equations

• (_ : IsometricVAdd M Xᵃᵒᵖ) = (_ : IsometricVAdd M Xᵃᵒᵖ)

instance instIsometricSMulMulOppositeInstPseudoEMetricSpaceMulOppositeSmul {M : Type u} {X : Type w} [PseudoEMetricSpace X] [SMul M X] [IsometricSMul M X] : IsometricSMul M Xᵐᵒᵖ

Equations

• (_ : IsometricSMul M Xᵐᵒᵖ) = (_ : IsometricSMul M Xᵐᵒᵖ)

instance ULift.isometricVAdd {M : Type u} {X : Type w} [PseudoEMetricSpace X] [VAdd M X] [IsometricVAdd M X] : IsometricVAdd (ULift.{u_2, u} M) X

Equations

• (_ : IsometricVAdd (ULift.{u_2, u} M) X) = (_ : IsometricVAdd (ULift.{u_2, u} M) X)

instance ULift.isometricSMul {M : Type u} {X : Type w} [PseudoEMetricSpace X] [SMul M X] [IsometricSMul M X] : IsometricSMul (ULift.{u_2, u} M) X

Equations

• (_ : IsometricSMul (ULift.{u_2, u} M) X) = (_ : IsometricSMul (ULift.{u_2, u} M) X)

instance ULift.isometricVAdd' {M : Type u} {X : Type w} [PseudoEMetricSpace X] [VAdd M X] [IsometricVAdd M X] : IsometricVAdd M (ULift.{u_2, w} X)

Equations

• (_ : IsometricVAdd M (ULift.{u_2, w} X)) = (_ : IsometricVAdd M (ULift.{u_2, w} X))

instance ULift.isometricSMul' {M : Type u} {X : Type w} [PseudoEMetricSpace X] [SMul M X] [IsometricSMul M X] : IsometricSMul M (ULift.{u_2, w} X)

Equations

• (_ : IsometricSMul M (ULift.{u_2, w} X)) = (_ : IsometricSMul M (ULift.{u_2, w} X))

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

• (_ : IsometricVAdd M ((i : ι) → X i)) = (_ : IsometricVAdd M ((i : ι) → X i))

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

• (_ : IsometricSMul M ((i : ι) → X i)) = (_ : IsometricSMul M ((i : ι) → X i))

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

• (_ : IsometricVAdd ((i : ι) → M i) ((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

• (_ : IsometricSMul ((i : ι) → M i) ((i : ι) → X i)) = (_ : IsometricSMul ((i : ι) → M i) ((i : ι) → X i))

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

• (_ : IsometricVAdd ((i : ι) → M i)ᵃᵒᵖ ((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

• (_ : IsometricSMul ((i : ι) → M i)ᵐᵒᵖ ((i : ι) → M i)) = (_ : IsometricSMul ((i : ι) → M i)ᵐᵒᵖ ((i : ι) → M i))

instance Additive.isometricVAdd {M : Type u} {X : Type w} [PseudoEMetricSpace X] [SMul M X] [IsometricSMul M X] : IsometricVAdd (Additive M) X

Equations

• (_ : IsometricVAdd (Additive M) X) = (_ : IsometricVAdd (Additive M) X)

instance Additive.isometricVAdd' {M : Type u} [Mul M] [PseudoEMetricSpace M] [IsometricSMul M M] : IsometricVAdd (Additive M) (Additive M)

Equations

• (_ : IsometricVAdd (Additive M) (Additive M)) = (_ : IsometricVAdd (Additive M) (Additive M))

instance Additive.isometricVAdd'' {M : Type u} [Mul M] [PseudoEMetricSpace M] [IsometricSMul Mᵐᵒᵖ M] : IsometricVAdd (Additive M)ᵃᵒᵖ (Additive M)

Equations

• (_ : IsometricVAdd (Additive M)ᵃᵒᵖ (Additive M)) = (_ : IsometricVAdd (Additive M)ᵃᵒᵖ (Additive M))

instance Multiplicative.isometricSMul {M : Type u_2} {X : Type u_3} [VAdd M X] [PseudoEMetricSpace X] [IsometricVAdd M X] : IsometricSMul (Multiplicative M) X

Equations

• (_ : IsometricSMul (Multiplicative M) X) = (_ : IsometricSMul (Multiplicative M) X)

instance Multiplicative.isometricSMul' {M : Type u} [Add M] [PseudoEMetricSpace M] [IsometricVAdd M M] : IsometricSMul (Multiplicative M) (Multiplicative M)

Equations

• (_ : IsometricSMul (Multiplicative M) (Multiplicative M)) = (_ : IsometricSMul (Multiplicative M) (Multiplicative M))

instance Multiplicative.isometricVAdd'' {M : Type u} [Add M] [PseudoEMetricSpace M] [IsometricVAdd Mᵃᵒᵖ M] : IsometricSMul (Multiplicative M)ᵐᵒᵖ (Multiplicative M)

Equations

• (_ : IsometricSMul (Multiplicative M)ᵐᵒᵖ (Multiplicative M)) = (_ : IsometricSMul (Multiplicative M)ᵐᵒᵖ (Multiplicative M))