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

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

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

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

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

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

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

theorem IsometricVAdd.to_continuousConstVAdd.proof_1 (M : Type u_1) (X : Type u_2) [PseudoEMetricSpace X] [VAdd M X] [IsometricVAdd M X] : ContinuousConstVAdd M X

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

Equations

• IsometricVAdd.to_continuousConstVAdd = IsometricVAdd.to_continuousConstVAdd.proof_1

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

Equations

• IsometricSMul.to_continuousConstSMul = IsometricSMul.to_continuousConstSMul.proof_1

theorem IsometricVAdd.opposite_of_comm.proof_1 (M : Type u_1) (X : Type u_2) [PseudoEMetricSpace X] [VAdd M X] [VAdd Mᵃᵒᵖ X] [IsCentralVAdd M X] [IsometricVAdd M X] : IsometricVAdd 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.opposite_of_comm = IsometricVAdd.opposite_of_comm.proof_1

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.opposite_of_comm = IsometricSMul.opposite_of_comm.proof_1

@[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 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) : 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 => 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 => 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.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.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_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 => 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 : G), edist (c + b) (c + c) = edist b c) }

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

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

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 : G), edist (c * b) (c * c) = edist b c) }

@[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.addRight_toEquiv {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd Gᵃᵒᵖ G] (c : G) : (IsometryEquiv.addRight c).toEquiv = Equiv.addRight 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

@[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.mulRight_apply {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul Gᵐᵒᵖ G] (c : G) (x : G) : ↑(IsometryEquiv.mulRight 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⁻¹

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) }

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]

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.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.subRight_apply {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd Gᵃᵒᵖ G] (c : G) (b : G) : ↑(IsometryEquiv.subRight 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

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 : G), edist (c - b) (c - c) = edist b c) }

@[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_apply {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G] (c : G) (b : G) : ↑(IsometryEquiv.divLeft c) b = c / b

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

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 : G), edist (c / b) (c / c) = edist b c) }

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.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.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_toEquiv (G : Type v) [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G] : (IsometryEquiv.inv G).toEquiv = Equiv.inv G

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

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_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) : 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_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]

theorem EMetric.preimage_add_right_closedBall {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd Gᵃᵒᵖ G] (a : G) (b : G) (r : ENNReal) : (fun x => 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 => 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_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 : ℝ) : 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_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 : ℝ) : 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_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 instIsometricVAddSumPseudoEMetricSpaceMaxVadd.proof_1 {M : Type u_1} {X : Type u_2} {Y : Type u_3} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] [VAdd M X] [IsometricVAdd M X] [VAdd M Y] [IsometricVAdd M Y] : IsometricVAdd M (X × Y)

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

• @instIsometricVAddSumPseudoEMetricSpaceMaxVadd = @instIsometricVAddSumPseudoEMetricSpaceMaxVadd.proof_1

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

• @instIsometricSMulProdPseudoEMetricSpaceMaxSmul = @instIsometricSMulProdPseudoEMetricSpaceMaxSmul.proof_1

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

• @Prod.isometricVAdd' = @Prod.isometricVAdd'.proof_1

theorem Prod.isometricVAdd'.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [PseudoEMetricSpace M] [IsometricVAdd M M] [Add N] [PseudoEMetricSpace N] [IsometricVAdd N 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

• @Prod.isometricSMul' = @Prod.isometricSMul'.proof_1

theorem Prod.isometricVAdd''.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [PseudoEMetricSpace M] [IsometricVAdd Mᵃᵒᵖ M] [Add N] [PseudoEMetricSpace N] [IsometricVAdd Nᵃᵒᵖ N] : IsometricVAdd (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

• @Prod.isometricVAdd'' = @Prod.isometricVAdd''.proof_1

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

• @Prod.isometricSMul'' = @Prod.isometricSMul''.proof_1

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

Equations

• @AddUnits.isometricVAdd = @AddUnits.isometricVAdd.proof_1

theorem AddUnits.isometricVAdd.proof_1 {M : Type u_1} {X : Type u_2} [PseudoEMetricSpace X] [VAdd M X] [IsometricVAdd M X] [AddMonoid M] : 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

• @Units.isometricSMul = @Units.isometricSMul.proof_1

theorem instIsometricVAddAddOppositeInstPseudoEMetricSpaceAddOppositeVadd.proof_1 {M : Type u_1} {X : Type u_2} [PseudoEMetricSpace X] [VAdd M X] [IsometricVAdd M X] : IsometricVAdd M Xᵃᵒᵖ

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

Equations

• @instIsometricVAddAddOppositeInstPseudoEMetricSpaceAddOppositeVadd = @instIsometricVAddAddOppositeInstPseudoEMetricSpaceAddOppositeVadd.proof_1

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

Equations

• @instIsometricSMulMulOppositeInstPseudoEMetricSpaceMulOppositeSmul = @instIsometricSMulMulOppositeInstPseudoEMetricSpaceMulOppositeSmul.proof_1

theorem ULift.isometricVAdd.proof_1 {M : Type u_1} {X : Type u_2} [PseudoEMetricSpace X] [VAdd M X] [IsometricVAdd M X] : IsometricVAdd (ULift.{u_3, u_1} 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

• @ULift.isometricVAdd = @ULift.isometricVAdd.proof_1

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

• @ULift.isometricSMul = @ULift.isometricSMul.proof_1

theorem ULift.isometricVAdd'.proof_1 {M : Type u_1} {X : Type u_2} [PseudoEMetricSpace X] [VAdd M X] [IsometricVAdd M X] : IsometricVAdd M (ULift.{u_3, u_2} 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

• @ULift.isometricVAdd' = @ULift.isometricVAdd'.proof_1

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

• @ULift.isometricSMul' = @ULift.isometricSMul'.proof_1

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

• @instIsometricVAddForAllPseudoEMetricSpacePiInstVAdd = @instIsometricVAddForAllPseudoEMetricSpacePiInstVAdd.proof_1

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

• @instIsometricSMulForAllPseudoEMetricSpacePiInstSMul = @instIsometricSMulForAllPseudoEMetricSpacePiInstSMul.proof_1

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

• @Pi.isometricVAdd' = @Pi.isometricVAdd'.proof_1

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

• @Pi.isometricSMul' = @Pi.isometricSMul'.proof_1

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

• @Pi.isometricVAdd'' = @Pi.isometricVAdd''.proof_1

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

• @Pi.isometricSMul'' = @Pi.isometricSMul''.proof_1

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

Equations

• @Additive.isometricVAdd = @Additive.isometricVAdd.proof_1

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

Equations

• @Additive.isometricVAdd' = @Additive.isometricVAdd'.proof_1

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

Equations

• @Additive.isometricVAdd'' = @Additive.isometricVAdd''.proof_1

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

Equations

• @Multiplicative.isometricSMul = @Multiplicative.isometricSMul.proof_1

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

Equations

• @Multiplicative.isometricSMul' = @Multiplicative.isometricSMul'.proof_1

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

Equations

• @Multiplicative.isometricVAdd'' = @Multiplicative.isometricVAdd''.proof_1