# 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) [VAdd M X] :

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
class IsometricSMul (M : Type u) (X : Type w) [SMul M X] :

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
theorem isometry_vadd {M : Type u} (X : Type w) [VAdd M X] [] (c : M) :
Isometry fun (x : X) => c +ᵥ x
theorem isometry_smul {M : Type u} (X : Type w) [SMul M X] [] (c : M) :
Isometry fun (x : X) => c x
Equations
• =
instance IsometricSMul.to_continuousConstSMul (M : Type u) (X : Type w) [SMul M X] [] :
Equations
• =
instance IsometricVAdd.opposite_of_comm (M : Type u) (X : Type w) [VAdd M X] [VAdd Mᵃᵒᵖ X] [] [] :
Equations
• =
instance IsometricSMul.opposite_of_comm (M : Type u) (X : Type w) [SMul M X] [SMul Mᵐᵒᵖ X] [] [] :
Equations
• =
@[simp]
theorem edist_vadd_left {M : Type u} {X : Type w} [VAdd M X] [] (c : M) (x : X) (y : X) :
edist (c +ᵥ x) (c +ᵥ y) = edist x y
@[simp]
theorem edist_smul_left {M : Type u} {X : Type w} [SMul M X] [] (c : M) (x : X) (y : X) :
edist (c x) (c y) = edist x y
@[simp]
theorem ediam_vadd {M : Type u} {X : Type w} [VAdd M X] [] (c : M) (s : Set X) :
@[simp]
theorem ediam_smul {M : Type u} {X : Type w} [SMul M X] [] (c : M) (s : Set X) :
theorem isometry_add_left {M : Type u} [Add M] [] (a : M) :
Isometry fun (x : M) => a + x
theorem isometry_mul_left {M : Type u} [Mul M] [] (a : M) :
Isometry fun (x : M) => a * x
@[simp]
theorem edist_add_left {M : Type u} [Add M] [] (a : M) (b : M) (c : M) :
edist (a + b) (a + c) = edist b c
@[simp]
theorem edist_mul_left {M : Type u} [Mul M] [] (a : M) (b : M) (c : M) :
edist (a * b) (a * c) = edist b c
theorem isometry_add_right {M : Type u} [Add M] [] (a : M) :
Isometry fun (x : M) => x + a
theorem isometry_mul_right {M : Type u} [Mul M] [] (a : M) :
Isometry fun (x : M) => x * a
@[simp]
theorem edist_add_right {M : Type u} [Add M] [] (a : M) (b : M) (c : M) :
edist (a + c) (b + c) = edist a b
@[simp]
theorem edist_mul_right {M : Type u} [Mul M] [] (a : M) (b : M) (c : M) :
edist (a * c) (b * c) = edist a b
@[simp]
theorem edist_sub_right {M : Type u} [] [] (a : M) (b : M) (c : M) :
edist (a - c) (b - c) = edist a b
@[simp]
theorem edist_div_right {M : Type u} [] [] (a : M) (b : M) (c : M) :
edist (a / c) (b / c) = edist a b
@[simp]
theorem edist_neg_neg {G : Type v} [] [] [] (a : G) (b : G) :
edist (-a) (-b) = edist a b
@[simp]
theorem edist_inv_inv {G : Type v} [] [] [] (a : G) (b : G) :
= edist a b
theorem isometry_neg {G : Type v} [] [] [] :
Isometry Neg.neg
theorem isometry_inv {G : Type v} [] [] [] :
Isometry Inv.inv
theorem edist_neg {G : Type v} [] [] [] (x : G) (y : G) :
edist (-x) y = edist x (-y)
theorem edist_inv {G : Type v} [] [] [] (x : G) (y : G) :
@[simp]
theorem edist_sub_left {G : Type v} [] [] [] (a : G) (b : G) (c : G) :
edist (a - b) (a - c) = edist b c
@[simp]
theorem edist_div_left {G : Type v} [] [] [] (a : G) (b : G) (c : G) :
edist (a / b) (a / c) = edist b c
def IsometryEquiv.constVAdd {G : Type v} {X : Type w} [] [] [] (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
• = { toEquiv := , isometry_toFun := }
Instances For
theorem IsometryEquiv.constVAdd.proof_1 {G : Type u_2} {X : Type u_1} [] [] [] (c : G) :
Isometry fun (x : X) => c +ᵥ x
@[simp]
theorem IsometryEquiv.constSMul_apply {G : Type v} {X : Type w} [] [] [] (c : G) (x : X) :
= c x
@[simp]
theorem IsometryEquiv.constSMul_toEquiv {G : Type v} {X : Type w} [] [] [] (c : G) :
.toEquiv =
@[simp]
theorem IsometryEquiv.constVAdd_apply {G : Type v} {X : Type w} [] [] [] (c : G) (x : X) :
= c +ᵥ x
@[simp]
theorem IsometryEquiv.constVAdd_toEquiv {G : Type v} {X : Type w} [] [] [] (c : G) :
.toEquiv =
def IsometryEquiv.constSMul {G : Type v} {X : Type w} [] [] [] (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
• = { toEquiv := , isometry_toFun := }
Instances For
@[simp]
theorem IsometryEquiv.constVAdd_symm {G : Type v} {X : Type w} [] [] [] (c : G) :
@[simp]
theorem IsometryEquiv.constSMul_symm {G : Type v} {X : Type w} [] [] [] (c : G) :
theorem IsometryEquiv.addLeft.proof_1 {G : Type u_1} [] [] (c : G) (b : G) (c : G) :
edist (c✝ + b) (c✝ + c) = edist b c
def IsometryEquiv.addLeft {G : Type v} [] [] (c : G) :
G ≃ᵢ G

Addition y ↦ x + y as an IsometryEquiv.

Equations
• = { toEquiv := , isometry_toFun := }
Instances For
@[simp]
theorem IsometryEquiv.mulLeft_toEquiv {G : Type v} [] [] (c : G) :
.toEquiv =
@[simp]
theorem IsometryEquiv.addLeft_apply {G : Type v} [] [] (c : G) (x : G) :
= c + x
@[simp]
theorem IsometryEquiv.addLeft_toEquiv {G : Type v} [] [] (c : G) :
.toEquiv =
@[simp]
theorem IsometryEquiv.mulLeft_apply {G : Type v} [] [] (c : G) (x : G) :
= c * x
def IsometryEquiv.mulLeft {G : Type v} [] [] (c : G) :
G ≃ᵢ G

Multiplication y ↦ x * y as an IsometryEquiv.

Equations
• = { toEquiv := , isometry_toFun := }
Instances For
@[simp]
theorem IsometryEquiv.addLeft_symm {G : Type v} [] [] (x : G) :
@[simp]
theorem IsometryEquiv.mulLeft_symm {G : Type v} [] [] (x : G) :
def IsometryEquiv.addRight {G : Type v} [] [] (c : G) :
G ≃ᵢ G

Addition y ↦ y + x as an IsometryEquiv.

Equations
• = { toEquiv := , isometry_toFun := }
Instances For
theorem IsometryEquiv.addRight.proof_1 {G : Type u_1} [] [] (c : G) (a : G) (b : G) :
edist (a + c) (b + c) = edist a b
@[simp]
theorem IsometryEquiv.addRight_toEquiv {G : Type v} [] [] (c : G) :
.toEquiv =
@[simp]
theorem IsometryEquiv.mulRight_apply {G : Type v} [] [] (c : G) (x : G) :
= x * c
@[simp]
theorem IsometryEquiv.addRight_apply {G : Type v} [] [] (c : G) (x : G) :
= x + c
@[simp]
theorem IsometryEquiv.mulRight_toEquiv {G : Type v} [] [] (c : G) :
.toEquiv =
def IsometryEquiv.mulRight {G : Type v} [] [] (c : G) :
G ≃ᵢ G

Multiplication y ↦ y * x as an IsometryEquiv.

Equations
• = { toEquiv := , isometry_toFun := }
Instances For
@[simp]
theorem IsometryEquiv.addRight_symm {G : Type v} [] [] (x : G) :
@[simp]
theorem IsometryEquiv.mulRight_symm {G : Type v} [] [] (x : G) :
def IsometryEquiv.subRight {G : Type v} [] [] (c : G) :
G ≃ᵢ G

Subtraction y ↦ y - x as an IsometryEquiv.

Equations
• = { toEquiv := , isometry_toFun := }
Instances For
theorem IsometryEquiv.subRight.proof_1 {G : Type u_1} [] [] (c : G) (a : G) (b : G) :
edist (a - c) (b - c) = edist a b
@[simp]
theorem IsometryEquiv.divRight_apply {G : Type v} [] [] (c : G) (b : G) :
= b / c
@[simp]
theorem IsometryEquiv.subRight_apply {G : Type v} [] [] (c : G) (b : G) :
= b - c
@[simp]
theorem IsometryEquiv.divRight_toEquiv {G : Type v} [] [] (c : G) :
.toEquiv =
@[simp]
theorem IsometryEquiv.subRight_toEquiv {G : Type v} [] [] (c : G) :
.toEquiv =
def IsometryEquiv.divRight {G : Type v} [] [] (c : G) :
G ≃ᵢ G

Division y ↦ y / x as an IsometryEquiv.

Equations
• = { toEquiv := , isometry_toFun := }
Instances For
@[simp]
theorem IsometryEquiv.subRight_symm {G : Type v} [] [] (c : G) :
@[simp]
theorem IsometryEquiv.divRight_symm {G : Type v} [] [] (c : G) :
def IsometryEquiv.subLeft {G : Type v} [] [] [] (c : G) :
G ≃ᵢ G

Subtraction y ↦ x - y as an IsometryEquiv.

Equations
• = { toEquiv := , isometry_toFun := }
Instances For
@[simp]
theorem IsometryEquiv.subLeft_symm_apply {G : Type v} [] [] [] (c : G) (b : G) :
= -b + c
@[simp]
theorem IsometryEquiv.divLeft_symm_apply {G : Type v} [] [] [] (c : G) (b : G) :
= b⁻¹ * c
@[simp]
theorem IsometryEquiv.divLeft_toEquiv {G : Type v} [] [] [] (c : G) :
.toEquiv =
@[simp]
theorem IsometryEquiv.subLeft_toEquiv {G : Type v} [] [] [] (c : G) :
.toEquiv =
@[simp]
theorem IsometryEquiv.subLeft_apply {G : Type v} [] [] [] (c : G) (b : G) :
= c - b
@[simp]
theorem IsometryEquiv.divLeft_apply {G : Type v} [] [] [] (c : G) (b : G) :
= c / b
def IsometryEquiv.divLeft {G : Type v} [] [] [] (c : G) :
G ≃ᵢ G

Division y ↦ x / y as an IsometryEquiv.

Equations
• = { toEquiv := , isometry_toFun := }
Instances For
def IsometryEquiv.neg (G : Type v) [] [] [] :
G ≃ᵢ G

Negation x ↦ -x as an IsometryEquiv.

Equations
• = { toEquiv := , isometry_toFun := }
Instances For
@[simp]
theorem IsometryEquiv.inv_apply (G : Type v) [] [] [] :
∀ (a : G), a = a⁻¹
@[simp]
theorem IsometryEquiv.neg_apply (G : Type v) [] [] [] :
∀ (a : G), a = -a
@[simp]
theorem IsometryEquiv.neg_toEquiv (G : Type v) [] [] [] :
.toEquiv =
@[simp]
theorem IsometryEquiv.inv_toEquiv (G : Type v) [] [] [] :
.toEquiv =
def IsometryEquiv.inv (G : Type v) [] [] [] :
G ≃ᵢ G

Inversion x ↦ x⁻¹ as an IsometryEquiv.

Equations
• = { toEquiv := , isometry_toFun := }
Instances For
@[simp]
theorem IsometryEquiv.neg_symm (G : Type v) [] [] [] :
@[simp]
theorem IsometryEquiv.inv_symm (G : Type v) [] [] [] :
@[simp]
theorem EMetric.vadd_ball {G : Type v} {X : Type w} [] [] [] (c : G) (x : X) (r : ENNReal) :
@[simp]
theorem EMetric.smul_ball {G : Type v} {X : Type w} [] [] [] (c : G) (x : X) (r : ENNReal) :
c = EMetric.ball (c x) r
@[simp]
theorem EMetric.preimage_vadd_ball {G : Type v} {X : Type w} [] [] [] (c : G) (x : X) (r : ENNReal) :
(fun (x : X) => c +ᵥ x) ⁻¹' = EMetric.ball (-c +ᵥ x) r
@[simp]
theorem EMetric.preimage_smul_ball {G : Type v} {X : Type w} [] [] [] (c : G) (x : X) (r : ENNReal) :
(fun (x : X) => c x) ⁻¹' = EMetric.ball (c⁻¹ x) r
@[simp]
theorem EMetric.vadd_closedBall {G : Type v} {X : Type w} [] [] [] (c : G) (x : X) (r : ENNReal) :
@[simp]
theorem EMetric.smul_closedBall {G : Type v} {X : Type w} [] [] [] (c : G) (x : X) (r : ENNReal) :
@[simp]
theorem EMetric.preimage_vadd_closedBall {G : Type v} {X : Type w} [] [] [] (c : G) (x : X) (r : ENNReal) :
(fun (x : X) => c +ᵥ x) ⁻¹' = EMetric.closedBall (-c +ᵥ x) r
@[simp]
theorem EMetric.preimage_smul_closedBall {G : Type v} {X : Type w} [] [] [] (c : G) (x : X) (r : ENNReal) :
(fun (x : X) => c x) ⁻¹' = EMetric.closedBall (c⁻¹ x) r
@[simp]
theorem EMetric.preimage_add_left_ball {G : Type v} [] [] (a : G) (b : G) (r : ENNReal) :
(fun (x : G) => a + x) ⁻¹' = EMetric.ball (-a + b) r
@[simp]
theorem EMetric.preimage_mul_left_ball {G : Type v} [] [] (a : G) (b : G) (r : ENNReal) :
(fun (x : G) => a * x) ⁻¹' = EMetric.ball (a⁻¹ * b) r
@[simp]
theorem EMetric.preimage_add_right_ball {G : Type v} [] [] (a : G) (b : G) (r : ENNReal) :
(fun (x : G) => x + a) ⁻¹' = EMetric.ball (b - a) r
@[simp]
theorem EMetric.preimage_mul_right_ball {G : Type v} [] [] (a : G) (b : G) (r : ENNReal) :
(fun (x : G) => x * a) ⁻¹' = EMetric.ball (b / a) r
@[simp]
theorem EMetric.preimage_add_left_closedBall {G : Type v} [] [] (a : G) (b : G) (r : ENNReal) :
(fun (x : G) => a + x) ⁻¹' = EMetric.closedBall (-a + b) r
@[simp]
theorem EMetric.preimage_mul_left_closedBall {G : Type v} [] [] (a : G) (b : G) (r : ENNReal) :
(fun (x : G) => a * x) ⁻¹' = EMetric.closedBall (a⁻¹ * b) r
@[simp]
theorem EMetric.preimage_add_right_closedBall {G : Type v} [] [] (a : G) (b : G) (r : ENNReal) :
(fun (x : G) => x + a) ⁻¹' = EMetric.closedBall (b - a) r
@[simp]
theorem EMetric.preimage_mul_right_closedBall {G : Type v} [] [] (a : G) (b : G) (r : ENNReal) :
(fun (x : G) => x * a) ⁻¹' = EMetric.closedBall (b / a) r
@[simp]
theorem dist_vadd {M : Type u} {X : Type w} [VAdd M X] [] (c : M) (x : X) (y : X) :
dist (c +ᵥ x) (c +ᵥ y) = dist x y
@[simp]
theorem dist_smul {M : Type u} {X : Type w} [SMul M X] [] (c : M) (x : X) (y : X) :
dist (c x) (c y) = dist x y
@[simp]
theorem nndist_vadd {M : Type u} {X : Type w} [VAdd M X] [] (c : M) (x : X) (y : X) :
nndist (c +ᵥ x) (c +ᵥ y) = nndist x y
@[simp]
theorem nndist_smul {M : Type u} {X : Type w} [SMul M X] [] (c : M) (x : X) (y : X) :
nndist (c x) (c y) = nndist x y
@[simp]
theorem diam_vadd {M : Type u} {X : Type w} [VAdd M X] [] (c : M) (s : Set X) :
@[simp]
theorem diam_smul {M : Type u} {X : Type w} [SMul M X] [] (c : M) (s : Set X) :
@[simp]
theorem dist_add_left {M : Type u} [Add M] [] (a : M) (b : M) (c : M) :
dist (a + b) (a + c) = dist b c
@[simp]
theorem dist_mul_left {M : Type u} [Mul M] [] (a : M) (b : M) (c : M) :
dist (a * b) (a * c) = dist b c
@[simp]
theorem nndist_add_left {M : Type u} [Add M] [] (a : M) (b : M) (c : M) :
nndist (a + b) (a + c) = nndist b c
@[simp]
theorem nndist_mul_left {M : Type u} [Mul M] [] (a : M) (b : M) (c : M) :
nndist (a * b) (a * c) = nndist b c
@[simp]
theorem dist_add_right {M : Type u} [Add M] [] (a : M) (b : M) (c : M) :
dist (a + c) (b + c) = dist a b
@[simp]
theorem dist_mul_right {M : Type u} [Mul M] [] (a : M) (b : M) (c : M) :
dist (a * c) (b * c) = dist a b
@[simp]
theorem nndist_add_right {M : Type u} [Add M] [] (a : M) (b : M) (c : M) :
nndist (a + c) (b + c) = nndist a b
@[simp]
theorem nndist_mul_right {M : Type u} [Mul M] [] (a : M) (b : M) (c : M) :
nndist (a * c) (b * c) = nndist a b
@[simp]
theorem dist_sub_right {M : Type u} [] [] (a : M) (b : M) (c : M) :
dist (a - c) (b - c) = dist a b
@[simp]
theorem dist_div_right {M : Type u} [] [] (a : M) (b : M) (c : M) :
dist (a / c) (b / c) = dist a b
@[simp]
theorem nndist_sub_right {M : Type u} [] [] (a : M) (b : M) (c : M) :
nndist (a - c) (b - c) = nndist a b
@[simp]
theorem nndist_div_right {M : Type u} [] [] (a : M) (b : M) (c : M) :
nndist (a / c) (b / c) = nndist a b
@[simp]
theorem dist_neg_neg {G : Type v} [] [] [] (a : G) (b : G) :
dist (-a) (-b) = dist a b
@[simp]
theorem dist_inv_inv {G : Type v} [] [] [] (a : G) (b : G) :
@[simp]
theorem nndist_neg_neg {G : Type v} [] [] [] (a : G) (b : G) :
nndist (-a) (-b) = nndist a b
@[simp]
theorem nndist_inv_inv {G : Type v} [] [] [] (a : G) (b : G) :
= nndist a b
@[simp]
theorem dist_sub_left {G : Type v} [] [] [] (a : G) (b : G) (c : G) :
dist (a - b) (a - c) = dist b c
@[simp]
theorem dist_div_left {G : Type v} [] [] [] (a : G) (b : G) (c : G) :
dist (a / b) (a / c) = dist b c
@[simp]
theorem nndist_sub_left {G : Type v} [] [] [] (a : G) (b : G) (c : G) :
nndist (a - b) (a - c) = nndist b c
@[simp]
theorem nndist_div_left {G : Type v} [] [] [] (a : G) (b : G) (c : G) :
nndist (a / b) (a / c) = nndist b c
theorem Bornology.IsBounded.vadd {G : Type v} {X : Type w} [VAdd G X] [] {s : Set X} (hs : ) (c : G) :

Given an additive isometric action of G on X, the image of a bounded set in X under translation by c : G is bounded

theorem Bornology.IsBounded.smul {G : Type v} {X : Type w} [SMul G X] [] {s : Set X} (hs : ) (c : G) :

If G acts isometrically on X, then the image of a bounded set in X under scalar multiplication by c : G is bounded. See also Bornology.IsBounded.smul₀ for a similar lemma about normed spaces.

@[simp]
theorem Metric.vadd_ball {G : Type v} {X : Type w} [] [] [] (c : G) (x : X) (r : ) :
@[simp]
theorem Metric.smul_ball {G : Type v} {X : Type w} [] [] [] (c : G) (x : X) (r : ) :
c = Metric.ball (c x) r
@[simp]
theorem Metric.preimage_vadd_ball {G : Type v} {X : Type w} [] [] [] (c : G) (x : X) (r : ) :
(fun (x : X) => c +ᵥ x) ⁻¹' = Metric.ball (-c +ᵥ x) r
@[simp]
theorem Metric.preimage_smul_ball {G : Type v} {X : Type w} [] [] [] (c : G) (x : X) (r : ) :
(fun (x : X) => c x) ⁻¹' = Metric.ball (c⁻¹ x) r
@[simp]
theorem Metric.vadd_closedBall {G : Type v} {X : Type w} [] [] [] (c : G) (x : X) (r : ) :
@[simp]
theorem Metric.smul_closedBall {G : Type v} {X : Type w} [] [] [] (c : G) (x : X) (r : ) :
@[simp]
theorem Metric.preimage_vadd_closedBall {G : Type v} {X : Type w} [] [] [] (c : G) (x : X) (r : ) :
(fun (x : X) => c +ᵥ x) ⁻¹' = Metric.closedBall (-c +ᵥ x) r
@[simp]
theorem Metric.preimage_smul_closedBall {G : Type v} {X : Type w} [] [] [] (c : G) (x : X) (r : ) :
(fun (x : X) => c x) ⁻¹' = Metric.closedBall (c⁻¹ x) r
@[simp]
theorem Metric.vadd_sphere {G : Type v} {X : Type w} [] [] [] (c : G) (x : X) (r : ) :
@[simp]
theorem Metric.smul_sphere {G : Type v} {X : Type w} [] [] [] (c : G) (x : X) (r : ) :
@[simp]
theorem Metric.preimage_vadd_sphere {G : Type v} {X : Type w} [] [] [] (c : G) (x : X) (r : ) :
(fun (x : X) => c +ᵥ x) ⁻¹' = Metric.sphere (-c +ᵥ x) r
@[simp]
theorem Metric.preimage_smul_sphere {G : Type v} {X : Type w} [] [] [] (c : G) (x : X) (r : ) :
(fun (x : X) => c x) ⁻¹' = Metric.sphere (c⁻¹ x) r
@[simp]
theorem Metric.preimage_add_left_ball {G : Type v} [] [] (a : G) (b : G) (r : ) :
(fun (x : G) => a + x) ⁻¹' = Metric.ball (-a + b) r
@[simp]
theorem Metric.preimage_mul_left_ball {G : Type v} [] [] (a : G) (b : G) (r : ) :
(fun (x : G) => a * x) ⁻¹' = Metric.ball (a⁻¹ * b) r
@[simp]
theorem Metric.preimage_add_right_ball {G : Type v} [] [] (a : G) (b : G) (r : ) :
(fun (x : G) => x + a) ⁻¹' = Metric.ball (b - a) r
@[simp]
theorem Metric.preimage_mul_right_ball {G : Type v} [] [] (a : G) (b : G) (r : ) :
(fun (x : G) => x * a) ⁻¹' = Metric.ball (b / a) r
@[simp]
theorem Metric.preimage_add_left_closedBall {G : Type v} [] [] (a : G) (b : G) (r : ) :
(fun (x : G) => a + x) ⁻¹' = Metric.closedBall (-a + b) r
@[simp]
theorem Metric.preimage_mul_left_closedBall {G : Type v} [] [] (a : G) (b : G) (r : ) :
(fun (x : G) => a * x) ⁻¹' = Metric.closedBall (a⁻¹ * b) r
@[simp]
theorem Metric.preimage_add_right_closedBall {G : Type v} [] [] (a : G) (b : G) (r : ) :
(fun (x : G) => x + a) ⁻¹' = Metric.closedBall (b - a) r
@[simp]
theorem Metric.preimage_mul_right_closedBall {G : Type v} [] [] (a : G) (b : G) (r : ) :
(fun (x : G) => x * a) ⁻¹' = Metric.closedBall (b / a) r
instance instIsometricVAddSumPseudoEMetricSpaceMaxVadd {M : Type u} {X : Type w} {Y : Type u_1} [VAdd M X] [] [VAdd M Y] [] :
Equations
• =
instance instIsometricSMulProdPseudoEMetricSpaceMaxSmul {M : Type u} {X : Type w} {Y : Type u_1} [SMul M X] [] [SMul M Y] [] :
Equations
• =
instance Prod.isometricVAdd' {M : Type u} {N : Type u_2} [Add M] [] [Add N] [] :
IsometricVAdd (M × N) (M × N)
Equations
• =
instance Prod.isometricSMul' {M : Type u} {N : Type u_2} [Mul M] [] [Mul N] [] :
IsometricSMul (M × N) (M × N)
Equations
• =
instance Prod.isometricVAdd'' {M : Type u} {N : Type u_2} [Add M] [] [Add N] [] :
Equations
• =
instance Prod.isometricSMul'' {M : Type u} {N : Type u_2} [Mul M] [] [Mul N] [] :
Equations
• =
Equations
• =
instance Units.isometricSMul {M : Type u} {X : Type w} [SMul M X] [] [] :
Equations
• =
instance ULift.isometricVAdd {M : Type u} {X : Type w} [VAdd M X] [] :
Equations
• =
instance ULift.isometricSMul {M : Type u} {X : Type w} [SMul M X] [] :
Equations
• =
instance ULift.isometricVAdd' {M : Type u} {X : Type w} [VAdd M X] [] :
Equations
• =
instance ULift.isometricSMul' {M : Type u} {X : Type w} [SMul M X] [] :
Equations
• =
instance instIsometricVAddForAllPseudoEMetricSpacePiInstVAdd {M : Type u} {ι : Type u_3} {X : ιType u_2} [] [(i : ι) → VAdd M (X i)] [(i : ι) → PseudoEMetricSpace (X i)] [∀ (i : ι), IsometricVAdd M (X i)] :
IsometricVAdd M ((i : ι) → X i)
Equations
• =
instance instIsometricSMulForAllPseudoEMetricSpacePiInstSMul {M : Type u} {ι : Type u_3} {X : ιType u_2} [] [(i : ι) → SMul M (X i)] [(i : ι) → PseudoEMetricSpace (X i)] [∀ (i : ι), IsometricSMul M (X i)] :
IsometricSMul M ((i : ι) → X i)
Equations
• =
instance Pi.isometricVAdd' {ι : Type u_4} {M : ιType u_2} {X : ιType u_3} [] [(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_4} {M : ιType u_2} {X : ιType u_3} [] [(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_3} {M : ιType u_2} [] [(i : ι) → Add (M i)] [(i : ι) → PseudoEMetricSpace (M i)] [∀ (i : ι), IsometricVAdd (M i)ᵃᵒᵖ (M i)] :
IsometricVAdd ((i : ι) → M i)ᵃᵒᵖ ((i : ι) → M i)
Equations
• =
instance Pi.isometricSMul'' {ι : Type u_3} {M : ιType u_2} [] [(i : ι) → Mul (M i)] [(i : ι) → PseudoEMetricSpace (M i)] [∀ (i : ι), IsometricSMul (M i)ᵐᵒᵖ (M i)] :
IsometricSMul ((i : ι) → M i)ᵐᵒᵖ ((i : ι) → M i)
Equations
• =
instance Additive.isometricVAdd {M : Type u} {X : Type w} [SMul M X] [] :
Equations
• =