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

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

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

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

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

• ⋯ = ⋯

@[instance 100]

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

• ⋯ = ⋯

@[simp]

theorem edist_smul_left {M : Type u} {X : Type w} [PseudoEMetricSpace X] [SMul M X] [IsometricSMul 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] [IsometricVAdd 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] [IsometricSMul 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] [IsometricVAdd 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] [IsometricSMul M M] (a : M) : Isometry fun (x : M) => a * x

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

@[simp]

theorem edist_mul_left {M : Type u} [Mul M] [PseudoEMetricSpace M] [IsometricSMul 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] [IsometricVAdd 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] [IsometricSMul Mᵐᵒᵖ M] (a : M) : Isometry fun (x : M) => x * a

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

theorem edist_div_left {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] [IsometricSMul 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] [IsometricVAdd G G] [IsometricVAdd 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] [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 := ⋯ }

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 := ⋯ }

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

@[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.constSMul_symm {G : Type v} {X : Type w} [PseudoEMetricSpace X] [Group G] [MulAction G X] [IsometricSMul G X] (c : G) : (IsometryEquiv.constSMul c).symm = IsometryEquiv.constSMul c⁻¹

@[simp]

theorem IsometryEquiv.constVAdd_symm {G : Type v} {X : Type w} [PseudoEMetricSpace X] [AddGroup G] [AddAction G X] [IsometricVAdd G X] (c : G) : (IsometryEquiv.constVAdd c).symm = IsometryEquiv.constVAdd (-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 := ⋯ }

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 := ⋯ }

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

@[simp]

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

@[simp]

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

@[simp]

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

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 := ⋯ }

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 := ⋯ }

@[simp]

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

@[simp]

theorem IsometryEquiv.addRight_apply {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd Gᵃᵒᵖ G] (c x : G) : (IsometryEquiv.addRight 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.mulRight_symm {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul Gᵐᵒᵖ G] (x : G) : (IsometryEquiv.mulRight x).symm = IsometryEquiv.mulRight x⁻¹

@[simp]

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

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 := ⋯ }

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 := ⋯ }

@[simp]

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

@[simp]

theorem IsometryEquiv.divRight_apply {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul Gᵐᵒᵖ G] (c b : G) : (IsometryEquiv.divRight c) b = b / 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.divRight_symm {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul Gᵐᵒᵖ G] (c : G) : (IsometryEquiv.divRight c).symm = IsometryEquiv.mulRight c

@[simp]

theorem IsometryEquiv.subRight_symm {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd Gᵃᵒᵖ G] (c : G) : (IsometryEquiv.subRight c).symm = IsometryEquiv.addRight 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 := ⋯ }

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 := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

theorem IsometryEquiv.subLeft_symm_apply {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsometricVAdd G G] [IsometricVAdd Gᵃᵒᵖ G] (c b : G) : (IsometryEquiv.subLeft c).symm 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.divLeft_symm_apply {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G] (c b : G) : (IsometryEquiv.divLeft c).symm b = 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

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 := ⋯ }

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 := ⋯ }

@[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.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_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_symm (G : Type v) [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G] : (IsometryEquiv.inv G).symm = IsometryEquiv.inv G

@[simp]

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

@[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.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.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.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.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.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.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_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_mul_left_ball {G : Type v} [Group G] [PseudoEMetricSpace G] [IsometricSMul G G] (a b : G) (r : ENNReal) : (fun (x : G) => a * x) ⁻¹' EMetric.ball b r = EMetric.ball (a⁻¹ * b) r

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem dist_smul {M : Type u} {X : Type w} [PseudoMetricSpace X] [SMul M X] [IsometricSMul 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] [IsometricVAdd 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] [IsometricSMul 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] [IsometricVAdd 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] [IsometricSMul 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] [IsometricVAdd 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] [IsometricSMul 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] [IsometricVAdd 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] [IsometricSMul 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] [IsometricVAdd 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] [IsometricSMul 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] [IsometricVAdd 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] [IsometricSMul 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] [IsometricVAdd 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] [IsometricSMul 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] [IsometricVAdd 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] [IsometricSMul 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] [IsometricVAdd 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] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G] (a b : G) : dist a⁻¹ b⁻¹ = dist a b

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem dist_div_left {G : Type v} [Group G] [PseudoMetricSpace G] [IsometricSMul G G] [IsometricSMul 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] [IsometricVAdd G G] [IsometricVAdd 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] [IsometricSMul G G] [IsometricSMul 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] [IsometricVAdd G G] [IsometricVAdd 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] [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.

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

@[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.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.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.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.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.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.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.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.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.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.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_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_mul_left_ball {G : Type v} [Group G] [PseudoMetricSpace G] [IsometricSMul G G] (a b : G) (r : ℝ) : (fun (x : G) => a * x) ⁻¹' Metric.ball b r = Metric.ball (a⁻¹ * b) r

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance instIsometricSMulProd {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

• ⋯ = ⋯

instance instIsometricVAddSum {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

• ⋯ = ⋯

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

• ⋯ = ⋯

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

• ⋯ = ⋯

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

• ⋯ = ⋯

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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

• ⋯ = ⋯

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

• ⋯ = ⋯

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

• ⋯ = ⋯

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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance Pi.isometricVAdd' {ι : Type u_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

• ⋯ = ⋯

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

• ⋯ = ⋯

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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯