Mathlib.Topology.MetricSpace.IsometricSMul

IsIsometricVAdd structure

[PseudoEMetricSpace X] [VAdd M X]

Full source

/-- An additive action is isometric if each map `x ↦ c +ᵥ x` is an isometry. -/
class IsIsometricVAdd [PseudoEMetricSpace X] [VAdd M X] : Prop where
  protected isometry_vadd : ∀ c : M, Isometry ((c +ᵥ ·) : X → X)

Isometric additive action on a pseudo extended metric space

Informal description

An additive action of a type `M` on a pseudo extended metric space `X` is called isometric if for every element `c` in `M`, the map `x ↦ c +ᵥ x` is an isometry (i.e., it preserves distances).

IsIsometricSMul structure

[PseudoEMetricSpace X] [SMul M X]

Full source

/-- A multiplicative action is isometric if each map `x ↦ c • x` is an isometry. -/
@[to_additive]
class IsIsometricSMul [PseudoEMetricSpace X] [SMul M X] : Prop where
  protected isometry_smul : ∀ c : M, Isometry ((c • ·) : X → X)

Isometric scalar multiplication action

Informal description

A multiplicative action of a type `M` on a pseudo extended metric space `X` is called isometric if for every element `c` in `M`, the map `x ↦ c • x` is an isometry (i.e., it preserves distances).

isometry_smul theorem

 {M : Type u} (X : Type w) [PseudoEMetricSpace X] [SMul M X] [IsIsometricSMul M X] (c : M) : Isometry (c • · : X → X)

Full source

@[to_additive]
theorem isometry_smul {M : Type u} (X : Type w) [PseudoEMetricSpace X] [SMul M X]
    [IsIsometricSMul M X] (c : M) : Isometry (c • · : X → X) :=
  IsIsometricSMul.isometry_smul c

Isometric Property of Scalar Multiplication on Pseudo Extended Metric Spaces

Informal description

Let $X$ be a pseudo extended metric space equipped with a scalar multiplication action by a type $M$. If this action is isometric (i.e., for every $c \in M$, the map $x \mapsto c \cdot x$ preserves distances), then for any fixed $c \in M$, the function $x \mapsto c \cdot x$ is an isometry on $X$.

IsIsometricSMul.to_continuousConstSMul instance

[PseudoEMetricSpace X] [SMul M X] [IsIsometricSMul M X] : ContinuousConstSMul M X

Full source

@[to_additive]
instance (priority := 100) IsIsometricSMul.to_continuousConstSMul [PseudoEMetricSpace X] [SMul M X]
    [IsIsometricSMul M X] : ContinuousConstSMul M X :=
  ⟨fun c => (isometry_smul X c).continuous⟩

Isometric Actions are Continuously Scalable

Informal description

For any pseudo extended metric space $X$ with a scalar multiplication action by $M$, if the action is isometric (i.e., each scalar multiplication preserves distances), then the action is also continuous in the second variable for each fixed scalar.

IsIsometricSMul.opposite_of_comm instance

 [PseudoEMetricSpace X] [SMul M X] [SMul Mᵐᵒᵖ X] [IsCentralScalar M X] [IsIsometricSMul M X] : IsIsometricSMul Mᵐᵒᵖ X

Full source

@[to_additive]
instance (priority := 100) IsIsometricSMul.opposite_of_comm [PseudoEMetricSpace X] [SMul M X]
    [SMul Mᵐᵒᵖ X] [IsCentralScalar M X] [IsIsometricSMul M X] : IsIsometricSMul Mᵐᵒᵖ X :=
  ⟨fun c x y => by simpa only [← op_smul_eq_smul] using isometry_smul X c.unop x y⟩

Isometric Property of Opposite Scalar Multiplication in Central Actions

Informal description

Let $X$ be a pseudo extended metric space with a scalar multiplication action by a type $M$ and its multiplicative opposite $M^\text{op}$. If the action of $M$ on $X$ is isometric and central (i.e., $c \cdot x = x \cdot c$ for all $c \in M$ and $x \in X$), then the action of $M^\text{op}$ on $X$ is also isometric.

edist_smul_left theorem

[SMul M X] [IsIsometricSMul M X] (c : M) (x y : X) : edist (c • x) (c • y) = edist x y

Full source

@[to_additive (attr := simp)]
theorem edist_smul_left [SMul M X] [IsIsometricSMul M X] (c : M) (x y : X) :
    edist (c • x) (c • y) = edist x y :=
  isometry_smul X c x y

Isometric Scalar Multiplication Preserves Distance: $d(c \cdot x, c \cdot y) = d(x, y)$

Informal description

Let $X$ be a pseudo extended metric space with a scalar multiplication action by a type $M$. If this action is isometric, then for any $c \in M$ and any two points $x, y \in X$, the extended distance between $c \cdot x$ and $c \cdot y$ is equal to the extended distance between $x$ and $y$, i.e., $d(c \cdot x, c \cdot y) = d(x, y)$.

ediam_smul theorem

[SMul M X] [IsIsometricSMul M X] (c : M) (s : Set X) : EMetric.diam (c • s) = EMetric.diam s

Full source

@[to_additive (attr := simp)]
theorem ediam_smul [SMul M X] [IsIsometricSMul M X] (c : M) (s : Set X) :
    EMetric.diam (c • s) = EMetric.diam s :=
  (isometry_smul _ _).ediam_image s

Invariance of Extended Diameter under Isometric Scalar Multiplication

Informal description

Let $X$ be a pseudo extended metric space with a scalar multiplication action by a type $M$. If this action is isometric, then for any $c \in M$ and any subset $s \subseteq X$, the extended diameter of the scaled set $c \cdot s$ is equal to the extended diameter of $s$, i.e., $\text{diam}(c \cdot s) = \text{diam}(s)$.

isometry_mul_left theorem

[Mul M] [PseudoEMetricSpace M] [IsIsometricSMul M M] (a : M) : Isometry (a * ·)

Full source

@[to_additive]
theorem isometry_mul_left [Mul M] [PseudoEMetricSpace M] [IsIsometricSMul M M] (a : M) :
    Isometry (a * ·) :=
  isometry_smul M a

Left Multiplication by a Fixed Element is an Isometry in a Group with Left-Invariant Metric

Informal description

Let $M$ be a multiplicative group equipped with a pseudo extended metric space structure, and suppose the multiplicative action of $M$ on itself is isometric. Then for any fixed element $a \in M$, the left multiplication map $x \mapsto a * x$ is an isometry on $M$.

edist_mul_left theorem

[Mul M] [PseudoEMetricSpace M] [IsIsometricSMul M M] (a b c : M) : edist (a * b) (a * c) = edist b c

Full source

@[to_additive (attr := simp)]
theorem edist_mul_left [Mul M] [PseudoEMetricSpace M] [IsIsometricSMul M M] (a b c : M) :
    edist (a * b) (a * c) = edist b c :=
  isometry_mul_left a b c

Left-Invariance of Extended Distance under Multiplication: $\text{edist}(a * b, a * c) = \text{edist}(b, c)$

Informal description

Let $M$ be a multiplicative group equipped with a pseudo extended metric space structure, and suppose the multiplicative action of $M$ on itself is isometric. Then for any elements $a, b, c \in M$, the extended distance between $a * b$ and $a * c$ is equal to the extended distance between $b$ and $c$, i.e., $\text{edist}(a * b, a * c) = \text{edist}(b, c)$.

isometry_mul_right theorem

[Mul M] [PseudoEMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a : M) : Isometry fun x => x * a

Full source

@[to_additive]
theorem isometry_mul_right [Mul M] [PseudoEMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a : M) :
    Isometry fun x => x * a :=
  isometry_smul M (MulOpposite.op a)

Right Multiplication by a Fixed Element is an Isometry in a Group with Right-Invariant Metric

Informal description

Let $M$ be a multiplicative group equipped with a pseudo extended metric space structure, and suppose the multiplicative action of $M^\text{op}$ on $M$ is isometric. Then for any fixed element $a \in M$, the right multiplication map $x \mapsto x * a$ is an isometry on $M$.

edist_mul_right theorem

[Mul M] [PseudoEMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M) : edist (a * c) (b * c) = edist a b

Full source

@[to_additive (attr := simp)]
theorem edist_mul_right [Mul M] [PseudoEMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M) :
    edist (a * c) (b * c) = edist a b :=
  isometry_mul_right c a b

Right-Invariance of Extended Distance under Multiplication: $\text{edist}(a * c, b * c) = \text{edist}(a, b)$

Informal description

Let $M$ be a multiplicative group equipped with a pseudo extended metric space structure, and suppose the multiplicative action of $M^\text{op}$ on $M$ is isometric. Then for any elements $a, b, c \in M$, the extended distance between $a * c$ and $b * c$ is equal to the extended distance between $a$ and $b$, i.e., $\text{edist}(a * c, b * c) = \text{edist}(a, b)$.

edist_div_right theorem

[DivInvMonoid M] [PseudoEMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M) : edist (a / c) (b / c) = edist a b

Full source

@[to_additive (attr := simp)]
theorem edist_div_right [DivInvMonoid M] [PseudoEMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M]
    (a b c : M) : edist (a / c) (b / c) = edist a b := by
  simp only [div_eq_mul_inv, edist_mul_right]

Right-Invariance of Extended Distance under Division: $\text{edist}(a / c, b / c) = \text{edist}(a, b)$

Informal description

Let $M$ be a group equipped with a pseudo extended metric space structure, and suppose the multiplicative action of $M^\text{op}$ on $M$ is isometric. Then for any elements $a, b, c \in M$, the extended distance between $a / c$ and $b / c$ is equal to the extended distance between $a$ and $b$, i.e., $\text{edist}(a / c, b / c) = \text{edist}(a, b)$.

edist_inv_inv theorem

[PseudoEMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) : edist a⁻¹ b⁻¹ = edist a b

Full source

@[to_additive (attr := simp)]
theorem edist_inv_inv [PseudoEMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G]
    (a b : G) : edist a⁻¹ b⁻¹ = edist a b := by
  rw [← edist_mul_left a, ← edist_mul_right _ _ b, mul_inv_cancel, one_mul, inv_mul_cancel_right,
    edist_comm]

Inversion Preserves Extended Distance: $\text{edist}(a^{-1}, b^{-1}) = \text{edist}(a, b)$

Informal description

Let $G$ be a group equipped with a pseudo extended metric space structure, where both the left and right multiplicative actions of $G$ on itself are isometric. Then for any elements $a, b \in G$, the extended distance between their inverses equals the extended distance between the original elements, i.e., $\text{edist}(a^{-1}, b^{-1}) = \text{edist}(a, b)$.

isometry_inv theorem

[PseudoEMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] : Isometry (Inv.inv : G → G)

Full source

@[to_additive]
theorem isometry_inv [PseudoEMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] :
    Isometry (Inv.inv : G → G) :=
  edist_inv_inv

Inversion Is an Isometry in a Group with Isometric Actions

Informal description

Let $G$ be a group equipped with a pseudo extended metric space structure, where both the left and right multiplicative actions of $G$ on itself are isometric. Then the inversion map $\text{Inv.inv} : G \to G$ (i.e., $x \mapsto x^{-1}$) is an isometry, meaning it preserves the extended distance between any two points in $G$.

edist_inv theorem

[PseudoEMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] (x y : G) : edist x⁻¹ y = edist x y⁻¹

Full source

@[to_additive]
theorem edist_inv [PseudoEMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G]
    (x y : G) : edist x⁻¹ y = edist x y⁻¹ := by rw [← edist_inv_inv, inv_inv]

Inversion Symmetry of Extended Distance: $\text{edist}(x^{-1}, y) = \text{edist}(x, y^{-1})$

Informal description

Let $G$ be a group equipped with a pseudo extended metric space structure, where both the left and right multiplicative actions of $G$ on itself are isometric. Then for any elements $x, y \in G$, the extended distance between $x^{-1}$ and $y$ equals the extended distance between $x$ and $y^{-1}$, i.e., $\text{edist}(x^{-1}, y) = \text{edist}(x, y^{-1})$.

edist_div_left theorem

 [PseudoEMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] (a b c : G) : edist (a / b) (a / c) = edist b c

Full source

@[to_additive (attr := simp)]
theorem edist_div_left [PseudoEMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G]
    (a b c : G) : edist (a / b) (a / c) = edist b c := by
  rw [div_eq_mul_inv, div_eq_mul_inv, edist_mul_left, edist_inv_inv]

Left Division Preserves Extended Distance: $\text{edist}(a/b, a/c) = \text{edist}(b, c)$

Informal description

Let $G$ be a group equipped with a pseudo extended metric space structure, where both the left and right multiplicative actions of $G$ on itself are isometric. Then for any elements $a, b, c \in G$, the extended distance between $a/b$ and $a/c$ equals the extended distance between $b$ and $c$, i.e., $\text{edist}(a/b, a/c) = \text{edist}(b, c)$.

IsometryEquiv.constSMul definition

(c : G) : X ≃ᵢ X

Full source

/-- 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. -/
@[to_additive (attr := simps! toEquiv apply) "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."]
def constSMul (c : G) : X ≃ᵢ X where
  toEquiv := MulAction.toPerm c
  isometry_toFun := isometry_smul X c

Isometric equivalence induced by constant group action

Informal description

Given a group $G$ acting isometrically on a pseudo extended metric space $X$, the function $\text{IsometryEquiv.constSMul}(c)$ for $c \in G$ is the isometric equivalence of $X$ induced by the group action $x \mapsto c \cdot x$.

IsometryEquiv.constSMul_symm theorem

(c : G) : (constSMul c : X ≃ᵢ X).symm = constSMul c⁻¹

Full source

@[to_additive (attr := simp)]
theorem constSMul_symm (c : G) : (constSMul c : X ≃ᵢ X).symm = constSMul c⁻¹ :=
  ext fun _ => rfl

Inverse of Isometric Group Action Equals Action by Inverse Element

Informal description

For any element $c$ in a group $G$ acting isometrically on a pseudo extended metric space $X$, the inverse of the isometric equivalence induced by the group action $x \mapsto c \cdot x$ is equal to the isometric equivalence induced by the action of the inverse element $c^{-1}$, i.e., $(\text{constSMul}\, c)^{-1} = \text{constSMul}\, c^{-1}$.

IsometryEquiv.mulLeft definition

[IsIsometricSMul G G] (c : G) : G ≃ᵢ G

Full source

/-- Multiplication `y ↦ x * y` as an `IsometryEquiv`. -/
@[to_additive (attr := simps! apply toEquiv) "Addition `y ↦ x + y` as an `IsometryEquiv`."]
def mulLeft [IsIsometricSMul G G] (c : G) : G ≃ᵢ G where
  toEquiv := Equiv.mulLeft c
  isometry_toFun := edist_mul_left c

Isometric equivalence of left multiplication in a group

Informal description

Given a group $G$ with an isometric left multiplication action (i.e., the metric on $G$ is left-invariant), the left multiplication map $x \mapsto c \cdot x$ for any $c \in G$ is an isometric equivalence of $G$ with itself.

IsometryEquiv.mulLeft_symm theorem

[IsIsometricSMul G G] (x : G) : (mulLeft x).symm = IsometryEquiv.mulLeft x⁻¹

Full source

@[to_additive (attr := simp)]
theorem mulLeft_symm [IsIsometricSMul G G] (x : G) :
    (mulLeft x).symm = IsometryEquiv.mulLeft x⁻¹ :=
  constSMul_symm x

Inverse of Left Multiplication Isometry Equals Left Multiplication by Inverse Element

Informal description

Let $G$ be a group with a left-invariant metric (i.e., the action of $G$ on itself by left multiplication is isometric). For any element $x \in G$, the inverse of the isometric equivalence given by left multiplication by $x$ is equal to the isometric equivalence given by left multiplication by $x^{-1}$, i.e., $(\text{mulLeft}\, x)^{-1} = \text{mulLeft}\, x^{-1}$.

IsometryEquiv.mulRight definition

[IsIsometricSMul Gᵐᵒᵖ G] (c : G) : G ≃ᵢ G

Full source

/-- Multiplication `y ↦ y * x` as an `IsometryEquiv`. -/
@[to_additive (attr := simps! apply toEquiv) "Addition `y ↦ y + x` as an `IsometryEquiv`."]
def mulRight [IsIsometricSMul Gᵐᵒᵖ G] (c : G) : G ≃ᵢ G where
  toEquiv := Equiv.mulRight c
  isometry_toFun a b := edist_mul_right a b c

Isometric equivalence of right multiplication in a group

Informal description

Given a group $G$ with a right-invariant metric (i.e., the action of $G$ on itself by right multiplication is isometric), the right multiplication map $x \mapsto x \cdot c$ for any $c \in G$ is an isometric equivalence of $G$ with itself. This means that the map preserves distances, i.e., the distance between $x \cdot c$ and $y \cdot c$ is equal to the distance between $x$ and $y$ for all $x, y \in G$.

IsometryEquiv.mulRight_symm theorem

[IsIsometricSMul Gᵐᵒᵖ G] (x : G) : (mulRight x).symm = mulRight x⁻¹

Full source

@[to_additive (attr := simp)]
theorem mulRight_symm [IsIsometricSMul Gᵐᵒᵖ G] (x : G) : (mulRight x).symm = mulRight x⁻¹ :=
  ext fun _ => rfl

Inverse of Right Multiplication Isometry Equals Right Multiplication by Inverse Element

Informal description

Let $G$ be a group with a right-invariant metric (i.e., the action of $G$ on itself by right multiplication is isometric). For any element $x \in G$, the inverse of the isometric equivalence given by right multiplication by $x$ is equal to the isometric equivalence given by right multiplication by $x^{-1}$, i.e., $(\text{mulRight}\, x)^{-1} = \text{mulRight}\, x^{-1}$.

IsometryEquiv.divRight definition

[IsIsometricSMul Gᵐᵒᵖ G] (c : G) : G ≃ᵢ G

Full source

/-- Division `y ↦ y / x` as an `IsometryEquiv`. -/
@[to_additive (attr := simps! apply toEquiv) "Subtraction `y ↦ y - x` as an `IsometryEquiv`."]
def divRight [IsIsometricSMul Gᵐᵒᵖ G] (c : G) : G ≃ᵢ G where
  toEquiv := Equiv.divRight c
  isometry_toFun a b := edist_div_right a b c

Isometric right division map

Informal description

For a group $G$ with a right-invariant pseudo extended metric (i.e., $G$ acts on itself by right multiplication isometrically), the right division map $\text{divRight}_c : G \to G$ defined by $\text{divRight}_c(x) = x / c$ is an isometric equivalence (distance-preserving bijection).

IsometryEquiv.divRight_symm theorem

[IsIsometricSMul Gᵐᵒᵖ G] (c : G) : (divRight c).symm = mulRight c

Full source

@[to_additive (attr := simp)]
theorem divRight_symm [IsIsometricSMul Gᵐᵒᵖ G] (c : G) : (divRight c).symm = mulRight c :=
  ext fun _ => rfl

Inverse of Isometric Right Division Equals Isometric Right Multiplication

Informal description

For a group $G$ with a right-invariant pseudo extended metric (i.e., $G$ acts on itself by right multiplication isometrically), the inverse of the isometric right division map $\text{divRight}_c : G \to G$ (defined by $\text{divRight}_c(x) = x / c$) is equal to the isometric right multiplication map $\text{mulRight}_c : G \to G$ (defined by $\text{mulRight}_c(x) = x \cdot c$).

IsometryEquiv.divLeft definition

(c : G) : G ≃ᵢ G

Full source

/-- Division `y ↦ x / y` as an `IsometryEquiv`. -/
@[to_additive (attr := simps! apply symm_apply toEquiv)
  "Subtraction `y ↦ x - y` as an `IsometryEquiv`."]
def divLeft (c : G) : G ≃ᵢ G where
  toEquiv := Equiv.divLeft c
  isometry_toFun := edist_div_left c

Isometric left division map

Informal description

For an element $ c $ in a group $ G $ equipped with a pseudo extended metric space structure where both left and right multiplicative actions are isometric, the left division map $ \text{divLeft}_c : G \to G $ defined by $ \text{divLeft}_c(x) = c / x $ is an isometric equivalence (a bijective distance-preserving map).

IsometryEquiv.inv definition

: G ≃ᵢ G

Full source

/-- Inversion `x ↦ x⁻¹` as an `IsometryEquiv`. -/
@[to_additive (attr := simps! apply toEquiv) "Negation `x ↦ -x` as an `IsometryEquiv`."]
def inv : G ≃ᵢ G where
  toEquiv := Equiv.inv G
  isometry_toFun := edist_inv_inv

Isometric inversion on a group

Informal description

The inversion map $x \mapsto x^{-1}$ on a group $G$ equipped with a pseudo extended metric space structure, where both the left and right multiplicative actions of $G$ on itself are isometric, is an isometric equivalence (i.e., it is bijective and preserves distances).

IsometryEquiv.inv_symm theorem

: (inv G).symm = inv G

Full source

@[to_additive (attr := simp)] theorem inv_symm : (inv G).symm = inv G := rfl

Self-inverse Property of Isometric Inversion

Informal description

The inverse of the isometric inversion map on a group $G$ is itself, i.e., $(x \mapsto x^{-1})^{-1} = (x \mapsto x^{-1})$.

EMetric.smul_ball theorem

(c : G) (x : X) (r : ℝ≥0∞) : c • ball x r = ball (c • x) r

Full source

@[to_additive (attr := simp)]
theorem smul_ball (c : G) (x : X) (r : ℝ≥0∞) : c • ball x r = ball (c • x) r :=
  (IsometryEquiv.constSMul c).image_emetric_ball _ _

Isometric Group Action Preserves Open Balls

Informal description

Let $G$ be a group acting isometrically on a pseudo extended metric space $X$. For any element $c \in G$, point $x \in X$, and radius $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the image of the open ball $B(x,r)$ under the group action $c \cdot \_$ equals the open ball centered at $c \cdot x$ with the same radius, i.e., $$ c \cdot B(x,r) = B(c \cdot x, r). $$

EMetric.preimage_smul_ball theorem

(c : G) (x : X) (r : ℝ≥0∞) : (c • ·) ⁻¹' ball x r = ball (c⁻¹ • x) r

Full source

@[to_additive (attr := simp)]
theorem preimage_smul_ball (c : G) (x : X) (r : ℝ≥0∞) :
    (c • ·) ⁻¹' ball x r = ball (c⁻¹ • x) r := by
  rw [preimage_smul, smul_ball]

Preimage of Open Ball under Isometric Group Action Equals Open Ball of Inverse Action

Informal description

Let $G$ be a group acting isometrically on a pseudo extended metric space $X$. For any element $c \in G$, point $x \in X$, and radius $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the preimage of the open ball $B(x, r)$ under the group action $c \cdot \_$ is equal to the open ball centered at $c^{-1} \cdot x$ with the same radius, i.e., $$ \{y \in X \mid c \cdot y \in B(x, r)\} = B(c^{-1} \cdot x, r). $$

EMetric.smul_closedBall theorem

(c : G) (x : X) (r : ℝ≥0∞) : c • closedBall x r = closedBall (c • x) r

Full source

@[to_additive (attr := simp)]
theorem smul_closedBall (c : G) (x : X) (r : ℝ≥0∞) : c • closedBall x r = closedBall (c • x) r :=
  (IsometryEquiv.constSMul c).image_emetric_closedBall _ _

Isometric Action Preserves Closed Balls: $c \cdot \overline{B}(x, r) = \overline{B}(c \cdot x, r)$

Informal description

Let $G$ be a group acting isometrically on a pseudo extended metric space $X$. For any element $c \in G$, point $x \in X$, and radius $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the image of the closed ball $\overline{B}(x, r)$ under the group action $c \cdot \cdot$ is equal to the closed ball $\overline{B}(c \cdot x, r)$.

EMetric.preimage_smul_closedBall theorem

(c : G) (x : X) (r : ℝ≥0∞) : (c • ·) ⁻¹' closedBall x r = closedBall (c⁻¹ • x) r

Full source

@[to_additive (attr := simp)]
theorem preimage_smul_closedBall (c : G) (x : X) (r : ℝ≥0∞) :
    (c • ·) ⁻¹' closedBall x r = closedBall (c⁻¹ • x) r := by
  rw [preimage_smul, smul_closedBall]

Preimage of Closed Ball under Isometric Group Action: $(y \mapsto c \cdot y)^{-1}(\overline{B}(x, r)) = \overline{B}(c^{-1} \cdot x, r)$

Informal description

Let $G$ be a group acting isometrically on a pseudo extended metric space $X$. For any element $c \in G$, point $x \in X$, and radius $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the preimage of the closed ball $\overline{B}(x, r)$ under the group action $y \mapsto c \cdot y$ is equal to the closed ball $\overline{B}(c^{-1} \cdot x, r)$.

EMetric.preimage_mul_left_ball theorem

[IsIsometricSMul G G] (a b : G) (r : ℝ≥0∞) : (a * ·) ⁻¹' ball b r = ball (a⁻¹ * b) r

Full source

@[to_additive (attr := simp)]
theorem preimage_mul_left_ball [IsIsometricSMul G G] (a b : G) (r : ℝ≥0∞) :
    (a * ·) ⁻¹' ball b r = ball (a⁻¹ * b) r :=
  preimage_smul_ball a b r

Preimage of Open Ball under Left Multiplication in a Group with Left-Invariant Metric

Informal description

Let $G$ be a group with a left-invariant pseudo extended metric (i.e., the left multiplication action is isometric). For any elements $a, b \in G$ and radius $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the preimage of the open ball $B(b, r)$ under the left multiplication map $x \mapsto a * x$ is equal to the open ball $B(a^{-1} * b, r)$. In other words: $$ \{x \in G \mid a * x \in B(b, r)\} = B(a^{-1} * b, r). $$

EMetric.preimage_mul_right_ball theorem

[IsIsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ℝ≥0∞) : (fun x => x * a) ⁻¹' ball b r = ball (b / a) r

Full source

@[to_additive (attr := simp)]
theorem preimage_mul_right_ball [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ℝ≥0∞) :
    (fun x => x * a) ⁻¹' ball b r = ball (b / a) r := by
  rw [div_eq_mul_inv]
  exact preimage_smul_ball (MulOpposite.op a) b r

Preimage of Open Ball under Right Multiplication in a Group with Right-Invariant Metric

Informal description

Let $G$ be a group with a right-invariant pseudo extended metric (i.e., the right multiplication action is isometric). For any elements $a, b \in G$ and radius $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the preimage of the open ball $B(b, r)$ under the right multiplication map $x \mapsto x * a$ is equal to the open ball $B(b / a, r)$. In other words: $$ \{x \in G \mid x * a \in B(b, r)\} = B(b / a, r). $$

EMetric.preimage_mul_left_closedBall theorem

[IsIsometricSMul G G] (a b : G) (r : ℝ≥0∞) : (a * ·) ⁻¹' closedBall b r = closedBall (a⁻¹ * b) r

Full source

@[to_additive (attr := simp)]
theorem preimage_mul_left_closedBall [IsIsometricSMul G G] (a b : G) (r : ℝ≥0∞) :
    (a * ·) ⁻¹' closedBall b r = closedBall (a⁻¹ * b) r :=
  preimage_smul_closedBall a b r

Preimage of Closed Ball under Left Multiplication: $(x \mapsto a * x)^{-1}(\overline{B}(b, r)) = \overline{B}(a^{-1} * b, r)$

Informal description

Let $G$ be a group acting isometrically on itself via left multiplication. For any elements $a, b \in G$ and radius $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the preimage of the closed ball $\overline{B}(b, r)$ under the left multiplication map $x \mapsto a * x$ is equal to the closed ball $\overline{B}(a^{-1} * b, r)$.

EMetric.preimage_mul_right_closedBall theorem

 [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ℝ≥0∞) : (fun x => x * a) ⁻¹' closedBall b r = closedBall (b / a) r

Full source

@[to_additive (attr := simp)]
theorem preimage_mul_right_closedBall [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ℝ≥0∞) :
    (fun x => x * a) ⁻¹' closedBall b r = closedBall (b / a) r := by
  rw [div_eq_mul_inv]
  exact preimage_smul_closedBall (MulOpposite.op a) b r

Preimage of Closed Ball under Right Multiplication: $(x \mapsto x * a)^{-1}(\overline{B}(b, r)) = \overline{B}(b / a, r)$

Informal description

Let $G$ be a group with a right-invariant extended metric (i.e., $G$ acts isometrically on itself via right multiplication). For any elements $a, b \in G$ and radius $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the preimage of the closed ball $\overline{B}(b, r)$ under the right multiplication map $x \mapsto x * a$ is equal to the closed ball $\overline{B}(b / a, r)$.

dist_smul theorem

[PseudoMetricSpace X] [SMul M X] [IsIsometricSMul M X] (c : M) (x y : X) : dist (c • x) (c • y) = dist x y

Full source

@[to_additive (attr := simp)]
theorem dist_smul [PseudoMetricSpace X] [SMul M X] [IsIsometricSMul M X] (c : M) (x y : X) :
    dist (c • x) (c • y) = dist x y :=
  (isometry_smul X c).dist_eq x y

Distance Preservation under Isometric Scalar Multiplication: $\text{dist}(c \cdot x, c \cdot y) = \text{dist}(x, y)$

Informal description

Let $X$ be a pseudometric space equipped with a scalar multiplication action by a type $M$. If this action is isometric (i.e., for every $c \in M$, the map $x \mapsto c \cdot x$ preserves distances), then for any fixed $c \in M$ and any two points $x, y \in X$, the distance between $c \cdot x$ and $c \cdot y$ is equal to the distance between $x$ and $y$, i.e., $\text{dist}(c \cdot x, c \cdot y) = \text{dist}(x, y)$.

nndist_smul theorem

[PseudoMetricSpace X] [SMul M X] [IsIsometricSMul M X] (c : M) (x y : X) : nndist (c • x) (c • y) = nndist x y

Full source

@[to_additive (attr := simp)]
theorem nndist_smul [PseudoMetricSpace X] [SMul M X] [IsIsometricSMul M X] (c : M) (x y : X) :
    nndist (c • x) (c • y) = nndist x y :=
  (isometry_smul X c).nndist_eq x y

Preservation of Non-Negative Distance under Isometric Scalar Multiplication

Informal description

Let $X$ be a pseudometric space equipped with a scalar multiplication action by a type $M$ that is isometric. For any $c \in M$ and any points $x, y \in X$, the non-negative distance between $c \cdot x$ and $c \cdot y$ is equal to the non-negative distance between $x$ and $y$, i.e., $\text{nndist}(c \cdot x, c \cdot y) = \text{nndist}(x, y)$.

diam_smul theorem

[PseudoMetricSpace X] [SMul M X] [IsIsometricSMul M X] (c : M) (s : Set X) : Metric.diam (c • s) = Metric.diam s

Full source

@[to_additive (attr := simp)]
theorem diam_smul [PseudoMetricSpace X] [SMul M X] [IsIsometricSMul M X] (c : M) (s : Set X) :
    Metric.diam (c • s) = Metric.diam s :=
  (isometry_smul _ _).diam_image s

Diameter Preservation under Isometric Scalar Multiplication: $\text{diam}(c \cdot s) = \text{diam}(s)$

Informal description

Let $X$ be a pseudometric space equipped with a scalar multiplication action by a type $M$ that is isometric. For any $c \in M$ and any subset $s \subseteq X$, the diameter of the scaled set $c \cdot s$ is equal to the diameter of $s$, i.e., $\text{diam}(c \cdot s) = \text{diam}(s)$.

dist_mul_left theorem

[PseudoMetricSpace M] [Mul M] [IsIsometricSMul M M] (a b c : M) : dist (a * b) (a * c) = dist b c

Full source

@[to_additive (attr := simp)]
theorem dist_mul_left [PseudoMetricSpace M] [Mul M] [IsIsometricSMul M M] (a b c : M) :
    dist (a * b) (a * c) = dist b c :=
  dist_smul a b c

Left Multiplication Preserves Distance in Isometric Pseudometric Space

Informal description

Let $M$ be a pseudometric space equipped with a multiplication operation and an isometric scalar multiplication action by itself. Then for any elements $a, b, c \in M$, the distance between $a \cdot b$ and $a \cdot c$ equals the distance between $b$ and $c$, i.e., $\text{dist}(a \cdot b, a \cdot c) = \text{dist}(b, c)$.

nndist_mul_left theorem

[PseudoMetricSpace M] [Mul M] [IsIsometricSMul M M] (a b c : M) : nndist (a * b) (a * c) = nndist b c

Full source

@[to_additive (attr := simp)]
theorem nndist_mul_left [PseudoMetricSpace M] [Mul M] [IsIsometricSMul M M] (a b c : M) :
    nndist (a * b) (a * c) = nndist b c :=
  nndist_smul a b c

Left Multiplication Preserves Non-Negative Distance in Isometric Pseudometric Spaces

Informal description

Let $M$ be a pseudometric space equipped with a multiplication operation and an isometric scalar multiplication action by itself. For any elements $a, b, c \in M$, the non-negative distance between $a \cdot b$ and $a \cdot c$ is equal to the non-negative distance between $b$ and $c$, i.e., $\text{nndist}(a \cdot b, a \cdot c) = \text{nndist}(b, c)$.

dist_mul_right theorem

[Mul M] [PseudoMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M) : dist (a * c) (b * c) = dist a b

Full source

@[to_additive (attr := simp)]
theorem dist_mul_right [Mul M] [PseudoMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M) :
    dist (a * c) (b * c) = dist a b :=
  dist_smul (MulOpposite.op c) a b

Right Multiplication Preserves Distance in Pseudometric Spaces: $\text{dist}(a \cdot c, b \cdot c) = \text{dist}(a, b)$

Informal description

Let $M$ be a pseudometric space equipped with a multiplication operation. If the multiplicative action of $M^\text{op}$ on $M$ is isometric (i.e., right multiplication by any element preserves distances), then for any elements $a, b, c \in M$, the distance between $a \cdot c$ and $b \cdot c$ is equal to the distance between $a$ and $b$, i.e., $\text{dist}(a \cdot c, b \cdot c) = \text{dist}(a, b)$.

nndist_mul_right theorem

[PseudoMetricSpace M] [Mul M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M) : nndist (a * c) (b * c) = nndist a b

Full source

@[to_additive (attr := simp)]
theorem nndist_mul_right [PseudoMetricSpace M] [Mul M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M) :
    nndist (a * c) (b * c) = nndist a b :=
  nndist_smul (MulOpposite.op c) a b

Right Multiplication Preserves Non-Negative Distance in Pseudometric Spaces

Informal description

Let $M$ be a pseudometric space equipped with a multiplication operation and an isometric scalar multiplication action by its multiplicative opposite $M^\text{op}$. For any elements $a, b, c \in M$, the non-negative distance between $a \cdot c$ and $b \cdot c$ is equal to the non-negative distance between $a$ and $b$, i.e., $\text{nndist}(a \cdot c, b \cdot c) = \text{nndist}(a, b)$.

dist_div_right theorem

[DivInvMonoid M] [PseudoMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M) : dist (a / c) (b / c) = dist a b

Full source

@[to_additive (attr := simp)]
theorem dist_div_right [DivInvMonoid M] [PseudoMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M]
    (a b c : M) : dist (a / c) (b / c) = dist a b := by simp only [div_eq_mul_inv, dist_mul_right]

Right Division Preserves Distance in Pseudometric Spaces: $\text{dist}(a / c, b / c) = \text{dist}(a, b)$

Informal description

Let $M$ be a pseudometric space equipped with a division operation and an isometric right multiplication action by its multiplicative opposite $M^\text{op}$. Then for any elements $a, b, c \in M$, the distance between $a / c$ and $b / c$ equals the distance between $a$ and $b$, i.e., $\text{dist}(a / c, b / c) = \text{dist}(a, b)$.

nndist_div_right theorem

[DivInvMonoid M] [PseudoMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M) : nndist (a / c) (b / c) = nndist a b

Full source

@[to_additive (attr := simp)]
theorem nndist_div_right [DivInvMonoid M] [PseudoMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M]
    (a b c : M) : nndist (a / c) (b / c) = nndist a b := by
  simp only [div_eq_mul_inv, nndist_mul_right]

Right Division Preserves Non-Negative Distance in Pseudometric Spaces

Informal description

Let $M$ be a pseudometric space equipped with a division and inversion operation (i.e., a `DivInvMonoid`), and suppose the multiplicative opposite $M^\text{op}$ acts isometrically on $M$ via scalar multiplication. Then for any elements $a, b, c \in M$, the non-negative distance between $a/c$ and $b/c$ equals the non-negative distance between $a$ and $b$, i.e., $\text{nndist}(a/c, b/c) = \text{nndist}(a, b)$.

dist_inv_inv theorem

 [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) : dist a⁻¹ b⁻¹ = dist a b

Full source

@[to_additive (attr := simp)]
theorem dist_inv_inv [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G]
    [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) : dist a⁻¹ b⁻¹ = dist a b :=
  (IsometryEquiv.inv G).dist_eq a b

Distance Preservation under Inversion in a Group with Isometric Actions

Informal description

Let $G$ be a group equipped with a pseudometric space structure such that both the left and right multiplicative actions of $G$ on itself are isometric. Then for any elements $a, b \in G$, the distance between their inverses equals the distance between the original elements, i.e., $\text{dist}(a^{-1}, b^{-1}) = \text{dist}(a, b)$.

nndist_inv_inv theorem

 [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) : nndist a⁻¹ b⁻¹ = nndist a b

Full source

@[to_additive (attr := simp)]
theorem nndist_inv_inv [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G]
    [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) : nndist a⁻¹ b⁻¹ = nndist a b :=
  (IsometryEquiv.inv G).nndist_eq a b

Invariance of Non-Negative Distance under Inversion in Groups with Isometric Actions

Informal description

Let $G$ be a group equipped with a pseudometric space structure such that both the left and right multiplicative actions of $G$ on itself are isometric. Then for any elements $a, b \in G$, the non-negative distance between their inverses equals the non-negative distance between the original elements, i.e., $\text{nndist}(a^{-1}, b^{-1}) = \text{nndist}(a, b)$.

dist_div_left theorem

 [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] (a b c : G) :
  dist (a / b) (a / c) = dist b c

Full source

@[to_additive (attr := simp)]
theorem dist_div_left [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G]
    [IsIsometricSMul Gᵐᵒᵖ G] (a b c : G) : dist (a / b) (a / c) = dist b c := by
  simp [div_eq_mul_inv]

Left Division Preserves Distance in Groups with Isometric Actions

Informal description

Let $G$ be a group equipped with a pseudometric space structure such that both the left and right multiplicative actions of $G$ on itself are isometric. Then for any elements $a, b, c \in G$, the distance between $a/b$ and $a/c$ equals the distance between $b$ and $c$, i.e., $\text{dist}(a/b, a/c) = \text{dist}(b, c)$.

nndist_div_left theorem

 [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] (a b c : G) :
  nndist (a / b) (a / c) = nndist b c

Full source

@[to_additive (attr := simp)]
theorem nndist_div_left [Group G] [PseudoMetricSpace G] [IsIsometricSMul G G]
    [IsIsometricSMul Gᵐᵒᵖ G] (a b c : G) : nndist (a / b) (a / c) = nndist b c := by
  simp [div_eq_mul_inv]

Left Division Preserves Non-Negative Distance in Groups with Isometric Actions

Informal description

Let $G$ be a group equipped with a pseudometric space structure such that both the left and right multiplicative actions of $G$ on itself are isometric. Then for any elements $a, b, c \in G$, the non-negative distance between $a/b$ and $a/c$ equals the non-negative distance between $b$ and $c$, i.e., $\text{nndist}(a/b, a/c) = \text{nndist}(b, c)$.

Bornology.IsBounded.smul theorem

[PseudoMetricSpace X] [SMul G X] [IsIsometricSMul G X] {s : Set X} (hs : IsBounded s) (c : G) : IsBounded (c • s)

Full source

/-- 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. -/
@[to_additive "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 [PseudoMetricSpace X] [SMul G X] [IsIsometricSMul G X] {s : Set X}
    (hs : IsBounded s) (c : G) : IsBounded (c • s) :=
  (isometry_smul X c).lipschitz.isBounded_image hs

Boundedness of Images under Isometric Group Actions: $c \cdot s$ is bounded for bounded $s$

Informal description

Let $X$ be a pseudometric space equipped with an isometric scalar multiplication action by a group $G$. For any bounded subset $s \subseteq X$ and any element $c \in G$, the image of $s$ under scalar multiplication by $c$, denoted $c \cdot s$, is also bounded.

Metric.smul_ball theorem

(c : G) (x : X) (r : ℝ) : c • ball x r = ball (c • x) r

Full source

@[to_additive (attr := simp)]
theorem smul_ball (c : G) (x : X) (r : ℝ) : c • ball x r = ball (c • x) r :=
  (IsometryEquiv.constSMul c).image_ball _ _

Isometric Group Action Preserves Open Balls: $c \cdot \text{ball}(x, r) = \text{ball}(c \cdot x, r)$

Informal description

Let $G$ be a group acting isometrically on a pseudometric space $X$. For any element $c \in G$, point $x \in X$, and radius $r \in \mathbb{R}$, the image of the open ball $\text{ball}(x, r)$ under the group action $c \cdot$ equals the open ball centered at $c \cdot x$ with radius $r$, i.e., $$ c \cdot \text{ball}(x, r) = \text{ball}(c \cdot x, r). $$

Metric.preimage_smul_ball theorem

(c : G) (x : X) (r : ℝ) : (c • ·) ⁻¹' ball x r = ball (c⁻¹ • x) r

Full source

@[to_additive (attr := simp)]
theorem preimage_smul_ball (c : G) (x : X) (r : ℝ) : (c • ·) ⁻¹' ball x r = ball (c⁻¹ • x) r := by
  rw [preimage_smul, smul_ball]

Preimage of Open Ball under Isometric Group Action: $(c \cdot)^{-1} \text{ball}(x, r) = \text{ball}(c^{-1} \cdot x, r)$

Informal description

Let $G$ be a group acting isometrically on a pseudometric space $X$. For any element $c \in G$, point $x \in X$, and radius $r \in \mathbb{R}$, the preimage of the open ball $\text{ball}(x, r)$ under the map $y \mapsto c \cdot y$ is equal to the open ball centered at $c^{-1} \cdot x$ with radius $r$, i.e., $$ \{ y \in X \mid c \cdot y \in \text{ball}(x, r) \} = \text{ball}(c^{-1} \cdot x, r). $$

Metric.smul_closedBall theorem

(c : G) (x : X) (r : ℝ) : c • closedBall x r = closedBall (c • x) r

Full source

@[to_additive (attr := simp)]
theorem smul_closedBall (c : G) (x : X) (r : ℝ) : c • closedBall x r = closedBall (c • x) r :=
  (IsometryEquiv.constSMul c).image_closedBall _ _

Isometric Group Action Preserves Closed Balls: $c \cdot \overline{B}(x, r) = \overline{B}(c \cdot x, r)$

Informal description

Let $G$ be a group acting isometrically on a pseudometric space $X$. For any element $c \in G$, point $x \in X$, and radius $r \in \mathbb{R}$, the image of the closed ball $\overline{B}(x, r)$ under the group action $c \cdot (\cdot)$ is equal to the closed ball centered at $c \cdot x$ with radius $r$, i.e., $$ c \cdot \overline{B}(x, r) = \overline{B}(c \cdot x, r). $$

Metric.preimage_smul_closedBall theorem

(c : G) (x : X) (r : ℝ) : (c • ·) ⁻¹' closedBall x r = closedBall (c⁻¹ • x) r

Full source

@[to_additive (attr := simp)]
theorem preimage_smul_closedBall (c : G) (x : X) (r : ℝ) :
    (c • ·) ⁻¹' closedBall x r = closedBall (c⁻¹ • x) r := by rw [preimage_smul, smul_closedBall]

Preimage of Closed Ball under Isometric Group Action: $(c \cdot \cdot)^{-1}(\overline{B}(x, r)) = \overline{B}(c^{-1} \cdot x, r)$

Informal description

Let $G$ be a group acting isometrically on a pseudometric space $X$. For any element $c \in G$, point $x \in X$, and radius $r \in \mathbb{R}$, the preimage of the closed ball $\overline{B}(x, r)$ under the left scalar multiplication by $c$ is equal to the closed ball centered at $c^{-1} \cdot x$ with radius $r$, i.e., \[ \{y \in X \mid c \cdot y \in \overline{B}(x, r)\} = \overline{B}(c^{-1} \cdot x, r). \]

Metric.smul_sphere theorem

(c : G) (x : X) (r : ℝ) : c • sphere x r = sphere (c • x) r

Full source

@[to_additive (attr := simp)]
theorem smul_sphere (c : G) (x : X) (r : ℝ) : c • sphere x r = sphere (c • x) r :=
  (IsometryEquiv.constSMul c).image_sphere _ _

Isometric Group Action Preserves Spheres

Informal description

Let $G$ be a group acting isometrically on a pseudometric space $X$. For any element $c \in G$, point $x \in X$, and radius $r \in \mathbb{R}$, the image of the sphere $\text{sphere}(x, r)$ under the group action $c \cdot (\cdot)$ is equal to the sphere centered at $c \cdot x$ with radius $r$, i.e., $$ c \cdot \text{sphere}(x, r) = \text{sphere}(c \cdot x, r). $$

Metric.preimage_smul_sphere theorem

(c : G) (x : X) (r : ℝ) : (c • ·) ⁻¹' sphere x r = sphere (c⁻¹ • x) r

Full source

@[to_additive (attr := simp)]
theorem preimage_smul_sphere (c : G) (x : X) (r : ℝ) :
    (c • ·) ⁻¹' sphere x r = sphere (c⁻¹ • x) r := by rw [preimage_smul, smul_sphere]

Preimage of Sphere under Isometric Group Action: $(c \cdot \cdot)^{-1}(S(x, r)) = S(c^{-1} \cdot x, r)$

Informal description

Let $G$ be a group acting isometrically on a pseudometric space $X$. For any element $c \in G$, point $x \in X$, and radius $r \in \mathbb{R}$, the preimage of the sphere $\text{sphere}(x, r)$ under the left scalar multiplication by $c$ is equal to the sphere centered at $c^{-1} \cdot x$ with radius $r$, i.e., \[ \{y \in X \mid c \cdot y \in \text{sphere}(x, r)\} = \text{sphere}(c^{-1} \cdot x, r). \]

Metric.preimage_mul_left_ball theorem

[IsIsometricSMul G G] (a b : G) (r : ℝ) : (a * ·) ⁻¹' ball b r = ball (a⁻¹ * b) r

Full source

@[to_additive (attr := simp)]
theorem preimage_mul_left_ball [IsIsometricSMul G G] (a b : G) (r : ℝ) :
    (a * ·) ⁻¹' ball b r = ball (a⁻¹ * b) r :=
  preimage_smul_ball a b r

Preimage of Open Ball under Left Multiplication in a Group with Left-Invariant Metric

Informal description

Let $G$ be a group acting isometrically on itself (i.e., with a left-invariant metric). For any elements $a, b \in G$ and radius $r \in \mathbb{R}$, the preimage of the open ball $\text{ball}(b, r)$ under left multiplication by $a$ is equal to the open ball centered at $a^{-1}b$ with radius $r$, i.e., $$ \{x \in G \mid a * x \in \text{ball}(b, r)\} = \text{ball}(a^{-1} * b, r). $$

Metric.preimage_mul_right_ball theorem

[IsIsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ℝ) : (fun x => x * a) ⁻¹' ball b r = ball (b / a) r

Full source

@[to_additive (attr := simp)]
theorem preimage_mul_right_ball [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ℝ) :
    (fun x => x * a) ⁻¹' ball b r = ball (b / a) r := by
  rw [div_eq_mul_inv]
  exact preimage_smul_ball (MulOpposite.op a) b r

Preimage of Open Ball under Right Multiplication in Right-Invariant Metric Group: $(x \mapsto x * a)^{-1}(\text{ball}(b, r)) = \text{ball}(b / a, r)$

Informal description

Let $G$ be a group with a right-invariant pseudometric (i.e., the right multiplication action by elements of $G$ is isometric). For any elements $a, b \in G$ and radius $r \in \mathbb{R}$, the preimage of the open ball $\text{ball}(b, r)$ under the right multiplication map $x \mapsto x * a$ is equal to the open ball centered at $b / a$ with radius $r$, i.e., $$ \{x \in G \mid x * a \in \text{ball}(b, r)\} = \text{ball}(b / a, r). $$

Metric.preimage_mul_left_closedBall theorem

[IsIsometricSMul G G] (a b : G) (r : ℝ) : (a * ·) ⁻¹' closedBall b r = closedBall (a⁻¹ * b) r

Full source

@[to_additive (attr := simp)]
theorem preimage_mul_left_closedBall [IsIsometricSMul G G] (a b : G) (r : ℝ) :
    (a * ·) ⁻¹' closedBall b r = closedBall (a⁻¹ * b) r :=
  preimage_smul_closedBall a b r

Preimage of Closed Ball under Left Multiplication in a Group with Left-Invariant Metric

Informal description

Let $G$ be a group acting isometrically on itself (with a left-invariant metric). For any elements $a, b \in G$ and radius $r \in \mathbb{R}$, the preimage of the closed ball $\overline{B}(b, r)$ under left multiplication by $a$ equals the closed ball centered at $a^{-1}b$ with radius $r$, i.e., \[ \{x \in G \mid a * x \in \overline{B}(b, r)\} = \overline{B}(a^{-1} * b, r). \]

Metric.preimage_mul_right_closedBall theorem

[IsIsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ℝ) : (fun x => x * a) ⁻¹' closedBall b r = closedBall (b / a) r

Full source

@[to_additive (attr := simp)]
theorem preimage_mul_right_closedBall [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ℝ) :
    (fun x => x * a) ⁻¹' closedBall b r = closedBall (b / a) r := by
  rw [div_eq_mul_inv]
  exact preimage_smul_closedBall (MulOpposite.op a) b r

Preimage of Closed Ball under Right Multiplication in Right-Invariant Metric Group: $(x \mapsto x * a)^{-1}(\overline{B}(b, r)) = \overline{B}(b / a, r)$

Informal description

Let $G$ be a group with a right-invariant pseudometric (i.e., $G^\text{op}$ acts isometrically on $G$ via right multiplication). For any elements $a, b \in G$ and radius $r \in \mathbb{R}$, the preimage of the closed ball $\overline{B}(b, r)$ under the right multiplication map $x \mapsto x * a$ equals the closed ball $\overline{B}(b / a, r)$. In other words: \[ \{x \in G \mid x * a \in \overline{B}(b, r)\} = \overline{B}(b / a, r). \]

Prod.instIsIsometricSMul instance

[SMul M Y] [IsIsometricSMul M Y] : IsIsometricSMul M (X × Y)

Full source

@[to_additive]
instance Prod.instIsIsometricSMul [SMul M Y] [IsIsometricSMul M Y] : IsIsometricSMul M (X × Y) :=
  ⟨fun c => (isometry_smul X c).prodMap (isometry_smul Y c)⟩

Isometric Scalar Multiplication on Product Spaces

Informal description

For any type $M$ acting on a pseudo extended metric space $Y$ by isometries, the product space $X \times Y$ inherits an isometric scalar multiplication action from $M$ on the second component.

Prod.isIsometricSMul' instance

 {N} [Mul M] [PseudoEMetricSpace M] [IsIsometricSMul M M] [Mul N] [PseudoEMetricSpace N] [IsIsometricSMul N N] :
  IsIsometricSMul (M × N) (M × N)

Full source

@[to_additive]
instance Prod.isIsometricSMul' {N} [Mul M] [PseudoEMetricSpace M] [IsIsometricSMul M M] [Mul N]
    [PseudoEMetricSpace N] [IsIsometricSMul N N] : IsIsometricSMul (M × N) (M × N) :=
  ⟨fun c => (isometry_smul M c.1).prodMap (isometry_smul N c.2)⟩

Isometric Scalar Multiplication on Product of Metric Spaces

Informal description

For any two pseudo extended metric spaces $M$ and $N$ equipped with multiplicative structures and isometric scalar multiplication actions on themselves, the product space $M \times N$ inherits an isometric scalar multiplication action from $M$ and $N$. This means that for any $(m, n) \in M \times N$, the map $(x, y) \mapsto (m \cdot x, n \cdot y)$ is an isometry on $M \times N$.

Prod.isIsometricSMul'' instance

 {N} [Mul M] [PseudoEMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] [Mul N] [PseudoEMetricSpace N] [IsIsometricSMul Nᵐᵒᵖ N] :
  IsIsometricSMul (M × N)ᵐᵒᵖ (M × N)

Full source

@[to_additive]
instance Prod.isIsometricSMul'' {N} [Mul M] [PseudoEMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M]
    [Mul N] [PseudoEMetricSpace N] [IsIsometricSMul Nᵐᵒᵖ N] :
    IsIsometricSMul (M × N)ᵐᵒᵖ (M × N) :=
  ⟨fun c => (isometry_mul_right c.unop.1).prodMap (isometry_mul_right c.unop.2)⟩

Isometric Action of Product Opposite on Product Space

Informal description

For any two pseudo extended metric spaces $M$ and $N$ equipped with multiplicative structures and isometric scalar multiplication actions of their multiplicative opposites on themselves, the multiplicative opposite of the product space $M \times N$ acts isometrically on $M \times N$. This means that for any $(m, n) \in (M \times N)^\text{op}$, the map $(x, y) \mapsto (m \cdot x, n \cdot y)$ is an isometry on $M \times N$.

Units.isIsometricSMul instance

[Monoid M] : IsIsometricSMul Mˣ X

Full source

@[to_additive]
instance Units.isIsometricSMul [Monoid M] : IsIsometricSMul Mˣ X :=
  ⟨fun c => isometry_smul X (c : M)⟩

Isometric Action by Units of a Monoid

Informal description

For any monoid $M$ acting on a pseudo extended metric space $X$ by isometries, the group of units $M^\times$ of $M$ also acts on $X$ by isometries. This means that for every invertible element $u \in M^\times$, the map $x \mapsto u \cdot x$ preserves distances in $X$.

instIsIsometricSMulMulOpposite instance

: IsIsometricSMul M Xᵐᵒᵖ

Full source

@[to_additive]
instance : IsIsometricSMul M Xᵐᵒᵖ :=
  ⟨fun c x y => by simpa only using edist_smul_left c x.unop y.unop⟩

Isometric Action on the Multiplicative Opposite of a Metric Space

Informal description

For any type $M$ acting isometrically on a pseudo extended metric space $X$, the multiplicative opposite $X^\text{op}$ also inherits an isometric action by $M$. This means that for every $c \in M$, the map $x \mapsto c \cdot x$ preserves distances in $X^\text{op}$.

ULift.isIsometricSMul instance

: IsIsometricSMul (ULift M) X

Full source

@[to_additive]
instance ULift.isIsometricSMul : IsIsometricSMul (ULift M) X :=
  ⟨fun c => by simpa only using isometry_smul X c.down⟩

Isometric Action by Lifted Type

Informal description

For any type $M$ acting on a pseudo extended metric space $X$ by isometries, the lifted type $\mathrm{ULift}\, M$ also acts on $X$ by isometries. This means that for every element $c$ in $\mathrm{ULift}\, M$, the map $x \mapsto c \cdot x$ preserves distances in $X$.

ULift.isIsometricSMul' instance

: IsIsometricSMul M (ULift X)

Full source

@[to_additive]
instance ULift.isIsometricSMul' : IsIsometricSMul M (ULift X) :=
  ⟨fun c x y => by simpa only using edist_smul_left c x.1 y.1⟩

Isometric Action on Lifted Metric Space

Informal description

For any type $M$ acting isometrically on a pseudo extended metric space $X$, the lifted space $\mathrm{ULift}\, X$ also inherits an isometric action by $M$. This means that for every $c \in M$, the map $x \mapsto c \cdot x$ preserves distances in $\mathrm{ULift}\, X$.

instIsIsometricSMulForall instance

 {ι} {X : ι → Type*} [Fintype ι] [∀ i, SMul M (X i)] [∀ i, PseudoEMetricSpace (X i)] [∀ i, IsIsometricSMul M (X i)] :
  IsIsometricSMul M (∀ i, X i)

Full source

@[to_additive]
instance {ι} {X : ι → Type*} [Fintype ι] [∀ i, SMul M (X i)] [∀ i, PseudoEMetricSpace (X i)]
    [∀ i, IsIsometricSMul M (X i)] : IsIsometricSMul M (∀ i, X i) :=
  ⟨fun c => .piMap (fun _ => (c • ·)) fun i => isometry_smul (X i) c⟩

Isometric Scalar Multiplication on Finite Product Spaces

Informal description

For a finite index set $\iota$ and a family of pseudo extended metric spaces $(X_i)_{i \in \iota}$ each equipped with a scalar multiplication action by $M$, if each action is isometric, then the pointwise scalar multiplication action of $M$ on the product space $\prod_{i \in \iota} X_i$ is also isometric.

Pi.isIsometricSMul' instance

 {ι} {M X : ι → Type*} [Fintype ι] [∀ i, SMul (M i) (X i)] [∀ i, PseudoEMetricSpace (X i)]
  [∀ i, IsIsometricSMul (M i) (X i)] : IsIsometricSMul (∀ i, M i) (∀ i, X i)

Full source

@[to_additive]
instance Pi.isIsometricSMul' {ι} {M X : ι → Type*} [Fintype ι] [∀ i, SMul (M i) (X i)]
    [∀ i, PseudoEMetricSpace (X i)] [∀ i, IsIsometricSMul (M i) (X i)] :
    IsIsometricSMul (∀ i, M i) (∀ i, X i) :=
  ⟨fun c => .piMap (fun i => (c i • ·)) fun _ => isometry_smul _ _⟩

Isometric Scalar Multiplication on Finite Product Spaces

Informal description

For a finite index set $\iota$ and families of types $(M_i)_{i \in \iota}$ and $(X_i)_{i \in \iota}$, where each $X_i$ is a pseudo extended metric space equipped with a scalar multiplication action by $M_i$, if each action is isometric (i.e., for every $c \in M_i$, the map $x \mapsto c \cdot x$ preserves distances), then the pointwise scalar multiplication action of $\prod_{i \in \iota} M_i$ on $\prod_{i \in \iota} X_i$ is also isometric.

Pi.isIsometricSMul'' instance

 {ι} {M : ι → Type*} [Fintype ι] [∀ i, Mul (M i)] [∀ i, PseudoEMetricSpace (M i)]
  [∀ i, IsIsometricSMul (M i)ᵐᵒᵖ (M i)] : IsIsometricSMul (∀ i, M i)ᵐᵒᵖ (∀ i, M i)

Full source

@[to_additive]
instance Pi.isIsometricSMul'' {ι} {M : ι → Type*} [Fintype ι] [∀ i, Mul (M i)]
    [∀ i, PseudoEMetricSpace (M i)] [∀ i, IsIsometricSMul (M i)ᵐᵒᵖ (M i)] :
    IsIsometricSMul (∀ i, M i)ᵐᵒᵖ (∀ i, M i) :=
  ⟨fun c => .piMap (fun i (x : M i) => x * c.unop i) fun _ => isometry_mul_right _⟩

Isometric Right Multiplication on Finite Product Groups

Informal description

For a finite index set $\iota$ and a family of multiplicative groups $(M_i)_{i \in \iota}$ each equipped with a pseudo extended metric space structure, if for each $i \in \iota$ the multiplicative action of $M_i^\text{op}$ on $M_i$ is isometric, then the pointwise multiplicative action of $\prod_{i \in \iota} M_i^\text{op}$ on $\prod_{i \in \iota} M_i$ is also isometric.

Additive.isIsIsometricVAdd instance

: IsIsometricVAdd (Additive M) X

Full source

instance Additive.isIsIsometricVAdd : IsIsometricVAdd (Additive M) X :=
  ⟨fun c => isometry_smul X c.toMul⟩

Isometric Additive Action from Isometric Multiplicative Action

Informal description

For any type $M$ with a multiplicative action on a pseudo extended metric space $X$ by isometries, the additive version of $M$ (denoted $\text{Additive}\, M$) has an additive action on $X$ by isometries.

Additive.isIsIsometricVAdd' instance

[Mul M] [PseudoEMetricSpace M] [IsIsometricSMul M M] : IsIsometricVAdd (Additive M) (Additive M)

Full source

instance Additive.isIsIsometricVAdd' [Mul M] [PseudoEMetricSpace M] [IsIsometricSMul M M] :
    IsIsometricVAdd (Additive M) (Additive M) :=
  ⟨fun c x y => edist_smul_left c.toMul x.toMul y.toMul⟩

Isometric Additive Action from Left-Invariant Multiplicative Action

Informal description

For any multiplicative group $M$ with a pseudo extended metric space structure and a left-invariant isometric scalar multiplication action (i.e., the action of $M$ on itself by left multiplication is isometric), the additive version of $M$ has an isometric additive action on itself.

Additive.isIsIsometricVAdd'' instance

[Mul M] [PseudoEMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] : IsIsometricVAdd (Additive M)ᵃᵒᵖ (Additive M)

Full source

instance Additive.isIsIsometricVAdd'' [Mul M] [PseudoEMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] :
    IsIsometricVAdd (Additive M)ᵃᵒᵖ (Additive M) :=
  ⟨fun c x y => edist_smul_left (MulOpposite.op c.unop.toMul) x.toMul y.toMul⟩

Isometric Additive Action from Right-Invariant Multiplicative Action

Informal description

For any multiplicative group $M$ with a pseudo extended metric space structure and a right-invariant isometric scalar multiplication action (i.e., the action of $M^\text{op}$ on $M$ by multiplication is isometric), the additive version of $M$ with the opposite addition operation has an isometric additive action on the additive version of $M$.

Multiplicative.isIsometricSMul instance

{M X} [VAdd M X] [PseudoEMetricSpace X] [IsIsometricVAdd M X] : IsIsometricSMul (Multiplicative M) X

Full source

instance Multiplicative.isIsometricSMul {M X} [VAdd M X] [PseudoEMetricSpace X]
    [IsIsometricVAdd M X] : IsIsometricSMul (Multiplicative M) X :=
  ⟨fun c => isometry_vadd X c.toAdd⟩

Isometric Multiplicative Action from Isometric Additive Action

Informal description

For any type $M$ with an additive action on a pseudo extended metric space $X$ that is isometric (i.e., the action preserves distances), the multiplicative version of $M$ (denoted $\text{Multiplicative } M$) has a multiplicative action on $X$ that is also isometric.

Multiplicative.isIsometricSMul' instance

[Add M] [PseudoEMetricSpace M] [IsIsometricVAdd M M] : IsIsometricSMul (Multiplicative M) (Multiplicative M)

Full source

instance Multiplicative.isIsometricSMul' [Add M] [PseudoEMetricSpace M] [IsIsometricVAdd M M] :
    IsIsometricSMul (Multiplicative M) (Multiplicative M) :=
  ⟨fun c x y => edist_vadd_left c.toAdd x.toAdd y.toAdd⟩

Isometric Multiplicative Action from Isometric Additive Self-Action

Informal description

For any additive group $M$ with a pseudo extended metric space structure, if the additive action of $M$ on itself is isometric, then the multiplicative version of $M$ (denoted $\text{Multiplicative } M$) has a multiplicative action on itself that is also isometric.

Multiplicative.isIsIsometricVAdd'' instance

 [Add M] [PseudoEMetricSpace M] [IsIsometricVAdd Mᵃᵒᵖ M] : IsIsometricSMul (Multiplicative M)ᵐᵒᵖ (Multiplicative M)

Full source

instance Multiplicative.isIsIsometricVAdd'' [Add M] [PseudoEMetricSpace M]
    [IsIsometricVAdd Mᵃᵒᵖ M] : IsIsometricSMul (Multiplicative M)ᵐᵒᵖ (Multiplicative M) :=
  ⟨fun c x y => edist_vadd_left (AddOpposite.op c.unop.toAdd) x.toAdd y.toAdd⟩

Isometric Action of Opposite Multiplicative Group on Multiplicative Group

Informal description

For any additive group $M$ with a pseudo extended metric space structure, if the additive action of the opposite group $M^\text{op}$ on $M$ is isometric, then the multiplicative action of the opposite multiplicative group $(\text{Multiplicative } M)^\text{op}$ on $\text{Multiplicative } M$ is also isometric.