Group actions by isometries

In this file we define two typeclasses:

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

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 IsIsometricSMul G G means that G has a left-invariant metric while IsIsometricSMul 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 IsIsometricVAdd (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

@[deprecated IsIsometricVAdd (since := "2025-03-10")]

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

Alias of IsIsometricVAdd.

---

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

class IsIsometricSMul (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

@[deprecated IsIsometricSMul (since := "2025-03-10")]

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

Alias of IsIsometricSMul.

---

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

theorem isometry_smul {M : Type u} (X : Type w) [PseudoEMetricSpace X] [SMul M X] [IsIsometricSMul M X] (c : M) : Isometry fun (x : X) => c • x

theorem isometry_vadd {M : Type u} (X : Type w) [PseudoEMetricSpace X] [VAdd M X] [IsIsometricVAdd M X] (c : M) : Isometry fun (x : X) => c +ᵥ x

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

@[simp]

theorem edist_smul_left {M : Type u} {X : Type w} [PseudoEMetricSpace X] [SMul M X] [IsIsometricSMul M X] (c : M) (x y : X) : edist (c • x) (c • y) = edist x y

@[simp]

theorem edist_vadd_left {M : Type u} {X : Type w} [PseudoEMetricSpace X] [VAdd M X] [IsIsometricVAdd M X] (c : M) (x y : X) : edist (c +ᵥ x) (c +ᵥ y) = edist x y

@[simp]

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

@[simp]

theorem ediam_vadd {M : Type u} {X : Type w} [PseudoEMetricSpace X] [VAdd M X] [IsIsometricVAdd M X] (c : M) (s : Set X) : EMetric.diam (c +ᵥ s) = EMetric.diam s

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

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

@[simp]

theorem edist_mul_left {M : Type u} [Mul M] [PseudoEMetricSpace M] [IsIsometricSMul M M] (a b c : M) : edist (a * b) (a * c) = edist b c

@[simp]

theorem edist_add_left {M : Type u} [Add M] [PseudoEMetricSpace M] [IsIsometricVAdd M M] (a b c : M) : edist (a + b) (a + c) = edist b c

theorem isometry_mul_right {M : Type u} [Mul M] [PseudoEMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a : M) : Isometry fun (x : M) => x * a

theorem isometry_add_right {M : Type u} [Add M] [PseudoEMetricSpace M] [IsIsometricVAdd Mᵃᵒᵖ M] (a : M) : Isometry fun (x : M) => x + a

@[simp]

theorem edist_mul_right {M : Type u} [Mul M] [PseudoEMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M) : edist (a * c) (b * c) = edist a b

@[simp]

theorem edist_add_right {M : Type u} [Add M] [PseudoEMetricSpace M] [IsIsometricVAdd Mᵃᵒᵖ M] (a b c : M) : edist (a + c) (b + c) = edist a b

@[simp]

theorem edist_div_right {M : Type u} [DivInvMonoid M] [PseudoEMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M) : edist (a / c) (b / c) = edist a b

@[simp]

theorem edist_sub_right {M : Type u} [SubNegMonoid M] [PseudoEMetricSpace M] [IsIsometricVAdd Mᵃᵒᵖ M] (a b c : M) : edist (a - c) (b - c) = edist a b

@[simp]

theorem edist_inv_inv {G : Type v} [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) : edist a⁻¹ b⁻¹ = edist a b

@[simp]

theorem edist_neg_neg {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsIsometricVAdd G G] [IsIsometricVAdd Gᵃᵒᵖ G] (a b : G) : edist (-a) (-b) = edist a b

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

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

theorem edist_inv {G : Type v} [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] (x y : G) : edist x⁻¹ y = edist x y⁻¹

theorem edist_neg {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsIsometricVAdd G G] [IsIsometricVAdd Gᵃᵒᵖ G] (x y : G) : edist (-x) y = edist x (-y)

@[simp]

theorem edist_div_left {G : Type v} [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] (a b c : G) : edist (a / b) (a / c) = edist b c

@[simp]

theorem edist_sub_left {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsIsometricVAdd G G] [IsIsometricVAdd Gᵃᵒᵖ G] (a b c : G) : edist (a - b) (a - c) = edist b c

def IsometryEquiv.constSMul {G : Type v} {X : Type w} [PseudoEMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul 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.

def IsometryEquiv.constVAdd {G : Type v} {X : Type w} [PseudoEMetricSpace X] [AddGroup G] [AddAction G X] [IsIsometricVAdd 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.

@[simp]

theorem IsometryEquiv.constSMul_apply {G : Type v} {X : Type w} [PseudoEMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] (c : G) (x : X) : (constSMul c) x = c • x

@[simp]

theorem IsometryEquiv.constVAdd_apply {G : Type v} {X : Type w} [PseudoEMetricSpace X] [AddGroup G] [AddAction G X] [IsIsometricVAdd G X] (c : G) (x : X) : (constVAdd c) x = c +ᵥ x

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Multiplication y ↦ x * y as an IsometryEquiv.

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

Addition y ↦ x + y as an IsometryEquiv.

@[simp]

theorem IsometryEquiv.mulLeft_apply {G : Type v} [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G G] (c x : G) : (mulLeft c) x = c * x

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Multiplication y ↦ y * x as an IsometryEquiv.

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

Addition y ↦ y + x as an IsometryEquiv.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Division y ↦ y / x as an IsometryEquiv.

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

Subtraction y ↦ y - x as an IsometryEquiv.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Division y ↦ x / y as an IsometryEquiv.

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

Subtraction y ↦ x - y as an IsometryEquiv.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Inversion x ↦ x⁻¹ as an IsometryEquiv.

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

Negation x ↦ -x as an IsometryEquiv.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem EMetric.smul_ball {G : Type v} {X : Type w} [PseudoEMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] (c : G) (x : X) (r : ENNReal) : c • ball x r = ball (c • x) r

@[simp]

theorem EMetric.vadd_ball {G : Type v} {X : Type w} [PseudoEMetricSpace X] [AddGroup G] [AddAction G X] [IsIsometricVAdd G X] (c : G) (x : X) (r : ENNReal) : c +ᵥ ball x r = ball (c +ᵥ x) r

@[simp]

theorem EMetric.preimage_smul_ball {G : Type v} {X : Type w} [PseudoEMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] (c : G) (x : X) (r : ENNReal) : (fun (x : X) => c • x) ⁻¹' ball x r = ball (c⁻¹ • x) r

@[simp]

theorem EMetric.preimage_vadd_ball {G : Type v} {X : Type w} [PseudoEMetricSpace X] [AddGroup G] [AddAction G X] [IsIsometricVAdd G X] (c : G) (x : X) (r : ENNReal) : (fun (x : X) => c +ᵥ x) ⁻¹' ball x r = ball (-c +ᵥ x) r

@[simp]

theorem EMetric.smul_closedBall {G : Type v} {X : Type w} [PseudoEMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] (c : G) (x : X) (r : ENNReal) : c • closedBall x r = closedBall (c • x) r

@[simp]

theorem EMetric.vadd_closedBall {G : Type v} {X : Type w} [PseudoEMetricSpace X] [AddGroup G] [AddAction G X] [IsIsometricVAdd G X] (c : G) (x : X) (r : ENNReal) : c +ᵥ closedBall x r = closedBall (c +ᵥ x) r

@[simp]

theorem EMetric.preimage_smul_closedBall {G : Type v} {X : Type w} [PseudoEMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] (c : G) (x : X) (r : ENNReal) : (fun (x : X) => c • x) ⁻¹' closedBall x r = closedBall (c⁻¹ • x) r

@[simp]

theorem EMetric.preimage_vadd_closedBall {G : Type v} {X : Type w} [PseudoEMetricSpace X] [AddGroup G] [AddAction G X] [IsIsometricVAdd G X] (c : G) (x : X) (r : ENNReal) : (fun (x : X) => c +ᵥ x) ⁻¹' closedBall x r = closedBall (-c +ᵥ x) r

@[simp]

theorem EMetric.preimage_mul_left_ball {G : Type v} [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G G] (a b : G) (r : ENNReal) : (fun (x : G) => a * x) ⁻¹' ball b r = ball (a⁻¹ * b) r

@[simp]

theorem EMetric.preimage_add_left_ball {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsIsometricVAdd G G] (a b : G) (r : ENNReal) : (fun (x : G) => a + x) ⁻¹' ball b r = ball (-a + b) r

@[simp]

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

@[simp]

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

@[simp]

theorem EMetric.preimage_mul_left_closedBall {G : Type v} [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G G] (a b : G) (r : ENNReal) : (fun (x : G) => a * x) ⁻¹' closedBall b r = closedBall (a⁻¹ * b) r

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem dist_smul {M : Type u} {X : Type w} [PseudoMetricSpace X] [SMul M X] [IsIsometricSMul M X] (c : M) (x y : X) : dist (c • x) (c • y) = dist x y

@[simp]

theorem dist_vadd {M : Type u} {X : Type w} [PseudoMetricSpace X] [VAdd M X] [IsIsometricVAdd M X] (c : M) (x y : X) : dist (c +ᵥ x) (c +ᵥ y) = dist x y

@[simp]

theorem nndist_smul {M : Type u} {X : Type w} [PseudoMetricSpace X] [SMul M X] [IsIsometricSMul M X] (c : M) (x y : X) : nndist (c • x) (c • y) = nndist x y

@[simp]

theorem nndist_vadd {M : Type u} {X : Type w} [PseudoMetricSpace X] [VAdd M X] [IsIsometricVAdd M X] (c : M) (x y : X) : nndist (c +ᵥ x) (c +ᵥ y) = nndist x y

@[simp]

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

@[simp]

theorem diam_vadd {M : Type u} {X : Type w} [PseudoMetricSpace X] [VAdd M X] [IsIsometricVAdd M X] (c : M) (s : Set X) : Metric.diam (c +ᵥ s) = Metric.diam s

@[simp]

theorem dist_mul_left {M : Type u} [PseudoMetricSpace M] [Mul M] [IsIsometricSMul M M] (a b c : M) : dist (a * b) (a * c) = dist b c

@[simp]

theorem dist_add_left {M : Type u} [PseudoMetricSpace M] [Add M] [IsIsometricVAdd M M] (a b c : M) : dist (a + b) (a + c) = dist b c

@[simp]

theorem nndist_mul_left {M : Type u} [PseudoMetricSpace M] [Mul M] [IsIsometricSMul M M] (a b c : M) : nndist (a * b) (a * c) = nndist b c

@[simp]

theorem nndist_add_left {M : Type u} [PseudoMetricSpace M] [Add M] [IsIsometricVAdd M M] (a b c : M) : nndist (a + b) (a + c) = nndist b c

@[simp]

theorem dist_mul_right {M : Type u} [Mul M] [PseudoMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M) : dist (a * c) (b * c) = dist a b

@[simp]

theorem dist_add_right {M : Type u} [Add M] [PseudoMetricSpace M] [IsIsometricVAdd Mᵃᵒᵖ M] (a b c : M) : dist (a + c) (b + c) = dist a b

@[simp]

theorem nndist_mul_right {M : Type u} [PseudoMetricSpace M] [Mul M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M) : nndist (a * c) (b * c) = nndist a b

@[simp]

theorem nndist_add_right {M : Type u} [PseudoMetricSpace M] [Add M] [IsIsometricVAdd Mᵃᵒᵖ M] (a b c : M) : nndist (a + c) (b + c) = nndist a b

@[simp]

theorem dist_div_right {M : Type u} [DivInvMonoid M] [PseudoMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M) : dist (a / c) (b / c) = dist a b

@[simp]

theorem dist_sub_right {M : Type u} [SubNegMonoid M] [PseudoMetricSpace M] [IsIsometricVAdd Mᵃᵒᵖ M] (a b c : M) : dist (a - c) (b - c) = dist a b

@[simp]

theorem nndist_div_right {M : Type u} [DivInvMonoid M] [PseudoMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M) : nndist (a / c) (b / c) = nndist a b

@[simp]

theorem nndist_sub_right {M : Type u} [SubNegMonoid M] [PseudoMetricSpace M] [IsIsometricVAdd Mᵃᵒᵖ M] (a b c : M) : nndist (a - c) (b - c) = nndist a b

@[simp]

theorem dist_inv_inv {G : Type v} [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) : dist a⁻¹ b⁻¹ = dist a b

@[simp]

theorem dist_neg_neg {G : Type v} [AddGroup G] [PseudoMetricSpace G] [IsIsometricVAdd G G] [IsIsometricVAdd Gᵃᵒᵖ G] (a b : G) : dist (-a) (-b) = dist a b

@[simp]

theorem nndist_inv_inv {G : Type v} [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) : nndist a⁻¹ b⁻¹ = nndist a b

@[simp]

theorem nndist_neg_neg {G : Type v} [AddGroup G] [PseudoMetricSpace G] [IsIsometricVAdd G G] [IsIsometricVAdd Gᵃᵒᵖ G] (a b : G) : nndist (-a) (-b) = nndist a b

@[simp]

theorem dist_div_left {G : Type v} [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] (a b c : G) : dist (a / b) (a / c) = dist b c

@[simp]

theorem dist_sub_left {G : Type v} [AddGroup G] [PseudoMetricSpace G] [IsIsometricVAdd G G] [IsIsometricVAdd Gᵃᵒᵖ G] (a b c : G) : dist (a - b) (a - c) = dist b c

@[simp]

theorem nndist_div_left {G : Type v} [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] (a b c : G) : nndist (a / b) (a / c) = nndist b c

@[simp]

theorem nndist_sub_left {G : Type v} [AddGroup G] [PseudoMetricSpace G] [IsIsometricVAdd G G] [IsIsometricVAdd Gᵃᵒᵖ G] (a b c : G) : nndist (a - b) (a - c) = nndist b c

theorem Bornology.IsBounded.smul {G : Type v} {X : Type w} [PseudoMetricSpace X] [SMul G X] [IsIsometricSMul G X] {s : Set X} (hs : IsBounded s) (c : G) : 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.

theorem Bornology.IsBounded.vadd {G : Type v} {X : Type w} [PseudoMetricSpace X] [VAdd G X] [IsIsometricVAdd G X] {s : Set X} (hs : IsBounded s) (c : G) : 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.

@[simp]

theorem Metric.smul_ball {G : Type v} {X : Type w} [PseudoMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] (c : G) (x : X) (r : ℝ) : c • ball x r = ball (c • x) r

@[simp]

theorem Metric.vadd_ball {G : Type v} {X : Type w} [PseudoMetricSpace X] [AddGroup G] [AddAction G X] [IsIsometricVAdd G X] (c : G) (x : X) (r : ℝ) : c +ᵥ ball x r = ball (c +ᵥ x) r

@[simp]

theorem Metric.preimage_smul_ball {G : Type v} {X : Type w} [PseudoMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] (c : G) (x : X) (r : ℝ) : (fun (x : X) => c • x) ⁻¹' ball x r = ball (c⁻¹ • x) r

@[simp]

theorem Metric.preimage_vadd_ball {G : Type v} {X : Type w} [PseudoMetricSpace X] [AddGroup G] [AddAction G X] [IsIsometricVAdd G X] (c : G) (x : X) (r : ℝ) : (fun (x : X) => c +ᵥ x) ⁻¹' ball x r = ball (-c +ᵥ x) r

@[simp]

theorem Metric.smul_closedBall {G : Type v} {X : Type w} [PseudoMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] (c : G) (x : X) (r : ℝ) : c • closedBall x r = closedBall (c • x) r

@[simp]

theorem Metric.vadd_closedBall {G : Type v} {X : Type w} [PseudoMetricSpace X] [AddGroup G] [AddAction G X] [IsIsometricVAdd G X] (c : G) (x : X) (r : ℝ) : c +ᵥ closedBall x r = closedBall (c +ᵥ x) r

@[simp]

theorem Metric.preimage_smul_closedBall {G : Type v} {X : Type w} [PseudoMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] (c : G) (x : X) (r : ℝ) : (fun (x : X) => c • x) ⁻¹' closedBall x r = closedBall (c⁻¹ • x) r

@[simp]

theorem Metric.preimage_vadd_closedBall {G : Type v} {X : Type w} [PseudoMetricSpace X] [AddGroup G] [AddAction G X] [IsIsometricVAdd G X] (c : G) (x : X) (r : ℝ) : (fun (x : X) => c +ᵥ x) ⁻¹' closedBall x r = closedBall (-c +ᵥ x) r

@[simp]

theorem Metric.smul_sphere {G : Type v} {X : Type w} [PseudoMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] (c : G) (x : X) (r : ℝ) : c • sphere x r = sphere (c • x) r

@[simp]

theorem Metric.vadd_sphere {G : Type v} {X : Type w} [PseudoMetricSpace X] [AddGroup G] [AddAction G X] [IsIsometricVAdd G X] (c : G) (x : X) (r : ℝ) : c +ᵥ sphere x r = sphere (c +ᵥ x) r

@[simp]

theorem Metric.preimage_smul_sphere {G : Type v} {X : Type w} [PseudoMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] (c : G) (x : X) (r : ℝ) : (fun (x : X) => c • x) ⁻¹' sphere x r = sphere (c⁻¹ • x) r

@[simp]

theorem Metric.preimage_vadd_sphere {G : Type v} {X : Type w} [PseudoMetricSpace X] [AddGroup G] [AddAction G X] [IsIsometricVAdd G X] (c : G) (x : X) (r : ℝ) : (fun (x : X) => c +ᵥ x) ⁻¹' sphere x r = sphere (-c +ᵥ x) r

@[simp]

theorem Metric.preimage_mul_left_ball {G : Type v} [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G] (a b : G) (r : ℝ) : (fun (x : G) => a * x) ⁻¹' ball b r = ball (a⁻¹ * b) r

@[simp]

theorem Metric.preimage_add_left_ball {G : Type v} [AddGroup G] [PseudoMetricSpace G] [IsIsometricVAdd G G] (a b : G) (r : ℝ) : (fun (x : G) => a + x) ⁻¹' ball b r = ball (-a + b) r

@[simp]

theorem Metric.preimage_mul_right_ball {G : Type v} [Group G] [PseudoMetricSpace G] [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ℝ) : (fun (x : G) => x * a) ⁻¹' ball b r = ball (b / a) r

@[simp]

theorem Metric.preimage_add_right_ball {G : Type v} [AddGroup G] [PseudoMetricSpace G] [IsIsometricVAdd Gᵃᵒᵖ G] (a b : G) (r : ℝ) : (fun (x : G) => x + a) ⁻¹' ball b r = ball (b - a) r

@[simp]

theorem Metric.preimage_mul_left_closedBall {G : Type v} [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G] (a b : G) (r : ℝ) : (fun (x : G) => a * x) ⁻¹' closedBall b r = closedBall (a⁻¹ * b) r

@[simp]

theorem Metric.preimage_add_left_closedBall {G : Type v} [AddGroup G] [PseudoMetricSpace G] [IsIsometricVAdd G G] (a b : G) (r : ℝ) : (fun (x : G) => a + x) ⁻¹' closedBall b r = closedBall (-a + b) r

@[simp]

theorem Metric.preimage_mul_right_closedBall {G : Type v} [Group G] [PseudoMetricSpace G] [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ℝ) : (fun (x : G) => x * a) ⁻¹' closedBall b r = closedBall (b / a) r

@[simp]

theorem Metric.preimage_add_right_closedBall {G : Type v} [AddGroup G] [PseudoMetricSpace G] [IsIsometricVAdd Gᵃᵒᵖ G] (a b : G) (r : ℝ) : (fun (x : G) => x + a) ⁻¹' closedBall b r = closedBall (b - a) r

instance Prod.instIsIsometricSMul {M : Type u} {X : Type w} {Y : Type u_1} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] [SMul M X] [IsIsometricSMul M X] [SMul M Y] [IsIsometricSMul M Y] : IsIsometricSMul M (X × Y)

instance Prod.instIsIsometricVAdd {M : Type u} {X : Type w} {Y : Type u_1} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] [VAdd M X] [IsIsometricVAdd M X] [VAdd M Y] [IsIsometricVAdd M Y] : IsIsometricVAdd M (X × Y)

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

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

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

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

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

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

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

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

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

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

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

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

instance instIsIsometricSMulForall {M : Type u} {ι : Type u_3} {X : ι → Type u_2} [Fintype ι] [(i : ι) → SMul M (X i)] [(i : ι) → PseudoEMetricSpace (X i)] [∀ (i : ι), IsIsometricSMul M (X i)] : IsIsometricSMul M ((i : ι) → X i)

instance instIsIsometricVAddForall {M : Type u} {ι : Type u_3} {X : ι → Type u_2} [Fintype ι] [(i : ι) → VAdd M (X i)] [(i : ι) → PseudoEMetricSpace (X i)] [∀ (i : ι), IsIsometricVAdd M (X i)] : IsIsometricVAdd M ((i : ι) → X i)

instance Pi.isIsometricSMul' {ι : Type u_4} {M : ι → Type u_2} {X : ι → Type u_3} [Fintype ι] [(i : ι) → SMul (M i) (X i)] [(i : ι) → PseudoEMetricSpace (X i)] [∀ (i : ι), IsIsometricSMul (M i) (X i)] : IsIsometricSMul ((i : ι) → M i) ((i : ι) → X i)

instance Pi.isIsometricVAdd' {ι : Type u_4} {M : ι → Type u_2} {X : ι → Type u_3} [Fintype ι] [(i : ι) → VAdd (M i) (X i)] [(i : ι) → PseudoEMetricSpace (X i)] [∀ (i : ι), IsIsometricVAdd (M i) (X i)] : IsIsometricVAdd ((i : ι) → M i) ((i : ι) → X i)

instance Pi.isIsometricSMul'' {ι : Type u_3} {M : ι → Type u_2} [Fintype ι] [(i : ι) → Mul (M i)] [(i : ι) → PseudoEMetricSpace (M i)] [∀ (i : ι), IsIsometricSMul (M i)ᵐᵒᵖ (M i)] : IsIsometricSMul ((i : ι) → M i)ᵐᵒᵖ ((i : ι) → M i)

instance Pi.isIsometricVAdd'' {ι : Type u_3} {M : ι → Type u_2} [Fintype ι] [(i : ι) → Add (M i)] [(i : ι) → PseudoEMetricSpace (M i)] [∀ (i : ι), IsIsometricVAdd (M i)ᵃᵒᵖ (M i)] : IsIsometricVAdd ((i : ι) → M i)ᵃᵒᵖ ((i : ι) → M i)

instance Additive.isIsIsometricVAdd {M : Type u} {X : Type w} [PseudoEMetricSpace X] [SMul M X] [IsIsometricSMul M X] : IsIsometricVAdd (Additive M) X

instance Additive.isIsIsometricVAdd' {M : Type u} [Mul M] [PseudoEMetricSpace M] [IsIsometricSMul M M] : IsIsometricVAdd (Additive M) (Additive M)

instance Additive.isIsIsometricVAdd'' {M : Type u} [Mul M] [PseudoEMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] : IsIsometricVAdd (Additive M)ᵃᵒᵖ (Additive M)

instance Multiplicative.isIsometricSMul {M : Type u_2} {X : Type u_3} [VAdd M X] [PseudoEMetricSpace X] [IsIsometricVAdd M X] : IsIsometricSMul (Multiplicative M) X

instance Multiplicative.isIsometricSMul' {M : Type u} [Add M] [PseudoEMetricSpace M] [IsIsometricVAdd M M] : IsIsometricSMul (Multiplicative M) (Multiplicative M)

instance Multiplicative.isIsIsometricVAdd'' {M : Type u} [Add M] [PseudoEMetricSpace M] [IsIsometricVAdd Mᵃᵒᵖ M] : IsIsometricSMul (Multiplicative M)ᵐᵒᵖ (Multiplicative M)