# 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`.

source
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

Instances

source
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

Instances

source
@[instance 100]
instance IsIsometricSMul.to_continuousConstSMul (M : Type u) (X : Type w) [PseudoEMetricSpace X] [SMul M X] [IsIsometricSMul M X] :
ContinuousConstSMul M X
source
@[instance 100]
instance IsIsometricVAdd.to_continuousConstVAdd (M : Type u) (X : Type w) [PseudoEMetricSpace X] [VAdd M X] [IsIsometricVAdd M X] :
ContinuousConstVAdd M X
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
theorem isometry_mul_left {M : Type u} [Mul M] [PseudoEMetricSpace M] [IsIsometricSMul M M] (a : M) :
Isometry fun (x : M) => a * x
source
theorem isometry_add_left {M : Type u} [Add M] [PseudoEMetricSpace M] [IsIsometricVAdd M M] (a : M) :
Isometry fun (x : M) => a + x
source
@[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
source
@[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
source
theorem isometry_mul_right {M : Type u} [Mul M] [PseudoEMetricSpace M] [IsIsometricSMul M ᵐᵒᵖ M] (a : M) :
Isometry fun (x : M) => x * a
source
theorem isometry_add_right {M : Type u} [Add M] [PseudoEMetricSpace M] [IsIsometricVAdd M ᵃᵒᵖ M] (a : M) :
Isometry fun (x : M) => x + a
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
theorem isometry_inv {G : Type v} [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul G ᵐᵒᵖ G] :
Isometry Inv.inv
source
theorem isometry_neg {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsIsometricVAdd G G] [IsIsometricVAdd G ᵃᵒᵖ G] :
Isometry Neg.neg
source
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⁻¹
source
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)
source
@[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
source
@[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
source
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.

Equations

- IsometryEquiv.constSMul c = { toEquiv := MulAction.toPerm c, isometry_toFun := ⋯ }

Instances For

source
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.

Equations

- IsometryEquiv.constVAdd c = { toEquiv := AddAction.toPerm c, isometry_toFun := ⋯ }

Instances For

source
@[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
source
@[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
source
@[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
source
@[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
source
@[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⁻¹
source
@[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)
source
def IsometryEquiv.mulLeft {G : Type v} [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G G] (c : G) :
G ≃ᵢ G

Multiplication `y ↦ x * y` as an `IsometryEquiv`.

Equations

- IsometryEquiv.mulLeft c = { toEquiv := Equiv.mulLeft c, isometry_toFun := ⋯ }

Instances For

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

Addition `y ↦ x + y` as an `IsometryEquiv`.

Equations

- IsometryEquiv.addLeft c = { toEquiv := Equiv.addLeft c, isometry_toFun := ⋯ }

Instances For

source
@[simp]
theorem IsometryEquiv.addLeft_apply {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsIsometricVAdd G G] (c x : G) :
(addLeft c) x = c + x
source
@[simp]
theorem IsometryEquiv.mulLeft_apply {G : Type v} [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G G] (c x : G) :
(mulLeft c) x = c * x
source
@[simp]
theorem IsometryEquiv.addLeft_toEquiv {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsIsometricVAdd G G] (c : G) :
(addLeft c).toEquiv = Equiv.addLeft c
source
@[simp]
theorem IsometryEquiv.mulLeft_toEquiv {G : Type v} [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G G] (c : G) :
(mulLeft c).toEquiv = Equiv.mulLeft c
source
@[simp]
theorem IsometryEquiv.mulLeft_symm {G : Type v} [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G G] (x : G) :
(mulLeft x).symm = mulLeft x⁻¹
source
@[simp]
theorem IsometryEquiv.addLeft_symm {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsIsometricVAdd G G] (x : G) :
(addLeft x).symm = addLeft (-x)
source
def IsometryEquiv.mulRight {G : Type v} [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G ᵐᵒᵖ G] (c : G) :
G ≃ᵢ G

Multiplication `y ↦ y * x` as an `IsometryEquiv`.

Equations

- IsometryEquiv.mulRight c = { toEquiv := Equiv.mulRight c, isometry_toFun := ⋯ }

Instances For

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

Addition `y ↦ y + x` as an `IsometryEquiv`.

Equations

- IsometryEquiv.addRight c = { toEquiv := Equiv.addRight c, isometry_toFun := ⋯ }

Instances For

source
@[simp]
theorem IsometryEquiv.addRight_apply {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsIsometricVAdd G ᵃᵒᵖ G] (c x : G) :
(addRight c) x = x + c
source
@[simp]
theorem IsometryEquiv.mulRight_apply {G : Type v} [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G ᵐᵒᵖ G] (c x : G) :
(mulRight c) x = x * c
source
@[simp]
theorem IsometryEquiv.mulRight_toEquiv {G : Type v} [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G ᵐᵒᵖ G] (c : G) :
(mulRight c).toEquiv = Equiv.mulRight c
source
@[simp]
theorem IsometryEquiv.addRight_toEquiv {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsIsometricVAdd G ᵃᵒᵖ G] (c : G) :
(addRight c).toEquiv = Equiv.addRight c
source
@[simp]
theorem IsometryEquiv.mulRight_symm {G : Type v} [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G ᵐᵒᵖ G] (x : G) :
(mulRight x).symm = mulRight x⁻¹
source
@[simp]
theorem IsometryEquiv.addRight_symm {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsIsometricVAdd G ᵃᵒᵖ G] (x : G) :
(addRight x).symm = addRight (-x)
source
def IsometryEquiv.divRight {G : Type v} [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G ᵐᵒᵖ G] (c : G) :
G ≃ᵢ G

Division `y ↦ y / x` as an `IsometryEquiv`.

Equations

- IsometryEquiv.divRight c = { toEquiv := Equiv.divRight c, isometry_toFun := ⋯ }

Instances For

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

Subtraction `y ↦ y - x` as an `IsometryEquiv`.

Equations

- IsometryEquiv.subRight c = { toEquiv := Equiv.subRight c, isometry_toFun := ⋯ }

Instances For

source
@[simp]
theorem IsometryEquiv.divRight_toEquiv {G : Type v} [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G ᵐᵒᵖ G] (c : G) :
(divRight c).toEquiv = Equiv.divRight c
source
@[simp]
theorem IsometryEquiv.divRight_apply {G : Type v} [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G ᵐᵒᵖ G] (c b : G) :
(divRight c) b = b / c
source
@[simp]
theorem IsometryEquiv.subRight_apply {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsIsometricVAdd G ᵃᵒᵖ G] (c b : G) :
(subRight c) b = b - c
source
@[simp]
theorem IsometryEquiv.subRight_toEquiv {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsIsometricVAdd G ᵃᵒᵖ G] (c : G) :
(subRight c).toEquiv = Equiv.subRight c
source
@[simp]
theorem IsometryEquiv.divRight_symm {G : Type v} [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G ᵐᵒᵖ G] (c : G) :
(divRight c).symm = mulRight c
source
@[simp]
theorem IsometryEquiv.subRight_symm {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsIsometricVAdd G ᵃᵒᵖ G] (c : G) :
(subRight c).symm = addRight c
source
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`.

Equations

- IsometryEquiv.divLeft c = { toEquiv := Equiv.divLeft c, isometry_toFun := ⋯ }

Instances For

source
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`.

Equations

- IsometryEquiv.subLeft c = { toEquiv := Equiv.subLeft c, isometry_toFun := ⋯ }

Instances For

source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
def IsometryEquiv.inv (G : Type v) [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul G ᵐᵒᵖ G] :
G ≃ᵢ G

Inversion `x ↦ x⁻¹` as an `IsometryEquiv`.

Equations

- IsometryEquiv.inv G = { toEquiv := Equiv.inv G, isometry_toFun := ⋯ }

Instances For

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

Negation `x ↦ -x` as an `IsometryEquiv`.

Equations

- IsometryEquiv.neg G = { toEquiv := Equiv.neg G, isometry_toFun := ⋯ }

Instances For

source
@[simp]
theorem IsometryEquiv.inv_toEquiv (G : Type v) [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul G ᵐᵒᵖ G] :
(inv G).toEquiv = Equiv.inv G
source
@[simp]
theorem IsometryEquiv.neg_apply (G : Type v) [AddGroup G] [PseudoEMetricSpace G] [IsIsometricVAdd G G] [IsIsometricVAdd G ᵃᵒᵖ G] (a✝ : G) :
(neg G) a✝ = -a✝
source
@[simp]
theorem IsometryEquiv.neg_toEquiv (G : Type v) [AddGroup G] [PseudoEMetricSpace G] [IsIsometricVAdd G G] [IsIsometricVAdd G ᵃᵒᵖ G] :
(neg G).toEquiv = Equiv.neg G
source
@[simp]
theorem IsometryEquiv.inv_apply (G : Type v) [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul G ᵐᵒᵖ G] (a✝ : G) :
(inv G) a✝ = a✝⁻¹
source
@[simp]
theorem IsometryEquiv.inv_symm (G : Type v) [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul G ᵐᵒᵖ G] :
(inv G).symm = inv G
source
@[simp]
theorem IsometryEquiv.neg_symm (G : Type v) [AddGroup G] [PseudoEMetricSpace G] [IsIsometricVAdd G G] [IsIsometricVAdd G ᵃᵒᵖ G] :
(neg G).symm = neg G
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
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.

source
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.

source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
instance Units.isIsometricSMul {M : Type u} {X : Type w} [PseudoEMetricSpace X] [SMul M X] [IsIsometricSMul M X] [Monoid M] :
IsIsometricSMul M ˣ X
source
instance AddUnits.isIsometricVAdd {M : Type u} {X : Type w} [PseudoEMetricSpace X] [VAdd M X] [IsIsometricVAdd M X] [AddMonoid M] :
IsIsometricVAdd (AddUnits M) X
source
instance instIsIsometricSMulMulOpposite {M : Type u} {X : Type w} [PseudoEMetricSpace X] [SMul M X] [IsIsometricSMul M X] :
IsIsometricSMul M X ᵐᵒᵖ
source
instance instIsIsometricVAddAddOpposite {M : Type u} {X : Type w} [PseudoEMetricSpace X] [VAdd M X] [IsIsometricVAdd M X] :
IsIsometricVAdd M X ᵃᵒᵖ
source
instance ULift.isIsometricSMul {M : Type u} {X : Type w} [PseudoEMetricSpace X] [SMul M X] [IsIsometricSMul M X] :
IsIsometricSMul (ULift.{u_2, u} M) X
source
instance ULift.isIsometricVAdd {M : Type u} {X : Type w} [PseudoEMetricSpace X] [VAdd M X] [IsIsometricVAdd M X] :
IsIsometricVAdd (ULift.{u_2, u} M) X
source
instance ULift.isIsometricSMul' {M : Type u} {X : Type w} [PseudoEMetricSpace X] [SMul M X] [IsIsometricSMul M X] :
IsIsometricSMul M (ULift.{u_2, w} X)
source
instance ULift.isIsometricVAdd' {M : Type u} {X : Type w} [PseudoEMetricSpace X] [VAdd M X] [IsIsometricVAdd M X] :
IsIsometricVAdd M (ULift.{u_2, w} X)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
instance Additive.isIsIsometricVAdd {M : Type u} {X : Type w} [PseudoEMetricSpace X] [SMul M X] [IsIsometricSMul M X] :
IsIsometricVAdd (Additive M) X
source
instance Additive.isIsIsometricVAdd' {M : Type u} [Mul M] [PseudoEMetricSpace M] [IsIsometricSMul M M] :
IsIsometricVAdd (Additive M) (Additive M)
source
instance Additive.isIsIsometricVAdd'' {M : Type u} [Mul M] [PseudoEMetricSpace M] [IsIsometricSMul M ᵐᵒᵖ M] :
IsIsometricVAdd (Additive M)ᵃᵒᵖ (Additive M)
source
instance Multiplicative.isIsometricSMul {M : Type u_2} {X : Type u_3} [VAdd M X] [PseudoEMetricSpace X] [IsIsometricVAdd M X] :
IsIsometricSMul (Multiplicative M) X
source
instance Multiplicative.isIsometricSMul' {M : Type u} [Add M] [PseudoEMetricSpace M] [IsIsometricVAdd M M] :
IsIsometricSMul (Multiplicative M) (Multiplicative M)
source
instance Multiplicative.isIsIsometricVAdd'' {M : Type u} [Add M] [PseudoEMetricSpace M] [IsIsometricVAdd M ᵃᵒᵖ M] :
IsIsometricSMul (Multiplicative M)ᵐᵒᵖ (Multiplicative M)