Metric.smul_closedBall
theorem Metric.smul_closedBall :
∀ {G : Type v} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : Group G] [inst_2 : MulAction G X]
[inst_3 : IsometricSMul G X] (c : G) (x : X) (r : ℝ), c • Metric.closedBall x r = Metric.closedBall (c • x) r
The theorem `Metric.smul_closedBall` states that for any pseudometric space `X`, any group `G`, and any action of `G` on `X` that is isometric, scalar multiplication of a closed ball in `X` with center `x` and radius `r` by an element `c` from `G` results in another closed ball with center `c • x` and the same radius `r`. In other words, the action of `G` scales the center of the closed ball without changing its radius or the distances between the points within the ball.
More concisely: For any pseudometric space X, group G acting isometrically on X, and closed ball B in X with center x and radius r, the scalar multiplication of B by c in G results in another closed ball with center c • x and radius r.
|
edist_add_right
theorem edist_add_right :
∀ {M : Type u} [inst : Add M] [inst_1 : PseudoEMetricSpace M] [inst_2 : IsometricVAdd Mᵃᵒᵖ M] (a b c : M),
edist (a + c) (b + c) = edist a b
This theorem, `edist_add_right`, states that for any type `M` that has an addition operation, forms a pseudo emetric space, and has an isometric action by addition, the extended distance (`edist`) between two elements `a` and `b` of `M` remains the same when a third element `c` is added to both `a` and `b`. In mathematical terms, `edist (a + c) (b + c) = edist a b`. This is equivalent to saying that the extended metric is translation invariant in this space.
More concisely: The extended metric `edist` on a type `M` with an addition operation, forming a pseudo metric space and preserving isometries, is translation invariant, i.e., `edist (a + c) (b + c) = edist a b` for all `a, b, c` in `M`.
|
Metric.smul_ball
theorem Metric.smul_ball :
∀ {G : Type v} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : Group G] [inst_2 : MulAction G X]
[inst_3 : IsometricSMul G X] (c : G) (x : X) (r : ℝ), c • Metric.ball x r = Metric.ball (c • x) r
The theorem `Metric.smul_ball` states that for any pseudometric space `X`, group `G` and multiplication action of `G` on `X` that is isometric, the scalar multiplication of a given element `c` from `G` with the metric ball of radius `r` around a point `x` in `X` results in the same set as the metric ball of radius `r` around the point obtained by the same scalar multiplication of `c` and `x`. In other words, the action of the group element `c` on the metric ball `Metric.ball x r` is equivalent to the action of `c` on the center `x` of the ball.
More concisely: For any pseudometric space X, group G acting isometrically on X, and point x in X, the metric balls with radius r centered at x and at the scalar multiplication of x by c in G are equal.
|
dist_vadd
theorem dist_vadd :
∀ {M : Type u} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : VAdd M X] [inst_2 : IsometricVAdd M X] (c : M)
(x y : X), dist (c +ᵥ x) (c +ᵥ y) = dist x y
This theorem states that for any types `M` and `X`, given that `X` is a pseudo metric space and `M` can be added to `X` in an isometric way (i.e., the addition preserves distances), then the distance between any two points `x` and `y` of type `X` will remain the same even after adding a constant `c` of type `M` to both points. In other words, in such a space, translating `x` and `y` by the same vector `c` does not change their distance.
More concisely: Given a pseudo metric space `X` and type `M` such that `M` can be isometrically added to `X`, the distance between any two points `x` and `y` in `X` is equal to the distance between `x + c` and `y + c` for any constant `c` of type `M`.
|
edist_add_left
theorem edist_add_left :
∀ {M : Type u} [inst : Add M] [inst_1 : PseudoEMetricSpace M] [inst_2 : IsometricVAdd M M] (a b c : M),
edist (a + b) (a + c) = edist b c
This theorem, `edist_add_left`, states that for any type `M` that has addition defined on it (`Add M`), is a pseudo-emetric space (`PseudoEMetricSpace M`), and supports isometric addition (`IsometricVAdd M M`), the edistance (extended distance) between the result of adding some elements `a` and `b`, and the result of adding the same `a` and `c`, equals the edistance between `b` and `c`. In other words, adding a fixed element `a` to both `b` and `c` does not change their relative distance in the associated metric space. This is a property of spaces that are translationally invariant, meaning the distances between points remain the same under translation.
More concisely: For any type `M` with Add, PseudoEMetricSpace, and IsometricVAdd, the edistance between `(a + b)` and `(a + c)` equals the edistance between `b` and `c` for all `a, b, c : M`.
|
dist_mul_right
theorem dist_mul_right :
∀ {M : Type u} [inst : Mul M] [inst_1 : PseudoMetricSpace M] [inst_2 : IsometricSMul Mᵐᵒᵖ M] (a b c : M),
dist (a * c) (b * c) = dist a b
This theorem states that for any type `M` that supports multiplication (`Mul`), is a pseudo metric space (`PseudoMetricSpace`), and has an isometric scalar multiplication (`IsometricSMul`) with its opposite (`Mᵐᵒᵖ`), the distance (`dist`) between the product of `a` and `c` and the product of `b` and `c` is equal to the distance between `a` and `b`. This essentially means that multiplication by a constant `c` doesn't affect the distance between two elements `a` and `b` in this space.
More concisely: For any type `M` with multiplication, being a pseudo metric space with isometric scalar multiplication by its opposite, the distance between the product of `a` and `c` and the product of `b` and `c` equals the distance between `a` and `b`.
|
edist_smul_left
theorem edist_smul_left :
∀ {M : Type u} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : SMul M X] [inst_2 : IsometricSMul M X] (c : M)
(x y : X), edist (c • x) (c • y) = edist x y
This theorem, `edist_smul_left`, states that for any types `M` and `X`, where `X` forms a pseudo-emetric space and `M` is capable of scalar multiplication on `X` such that the scalar multiplication is isometric (i.e., it preserves the distance), the extended distance (edist) between the scalar multiplication of a scalar `c` and `x` and the scalar multiplication of `c` and `y` is the same as the extended distance between `x` and `y`. In mathematical terms, for all `c`, `x`, and `y`, `edist (c • x) (c • y) = edist x y`.
More concisely: For any type `M` with scalar multiplication that preserves the pseudo-metric on `X`, the extended distance between `c • x` and `c • y` equals the extended distance between `x` and `y`, for all scalars `c` and elements `x`, `y` in `M`.
|
edist_mul_left
theorem edist_mul_left :
∀ {M : Type u} [inst : Mul M] [inst_1 : PseudoEMetricSpace M] [inst_2 : IsometricSMul M M] (a b c : M),
edist (a * b) (a * c) = edist b c
This theorem states that for any type `M` that is equipped with a multiplication operation, a pseudo emetric space structure, and an isometric scalar multiplication structure, the edistance (extended distance) between the product of `a` and `b` and the product of `a` and `c` is equal to the edistance between `b` and `c`. This essentially means the multiplication by `a` preserves the edistance between `b` and `c`. This is applicable for any elements `a`, `b` and `c` in `M`.
More concisely: For any type `M` with multiplication, a pseudo-metric, and isometric scalar multiplication, the extended distance between `a` \* `b` and `a` \* `c` equals the extended distance between `b` and `c`, for all `a, b, c` in `M`.
|
Bornology.IsBounded.smul
theorem Bornology.IsBounded.smul :
∀ {G : Type v} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : SMul G X] [inst_2 : IsometricSMul G X]
{s : Set X}, Bornology.IsBounded s → ∀ (c : G), Bornology.IsBounded (c • s)
This theorem states that if a set `G` acts isometrically on a set `X` (i.e., distance preserving scalar multiplication), then the image of a set `s` from `X` that is bounded (in the sense of the ambient bornology on `X`) remains bounded under scalar multiplication by any element `c` from `G`. This result also has a parallel in the context of normed spaces, as indicated by a reference to `Bornology.IsBounded.smul₀`, which asserts a similar property.
More concisely: If `G` acts isometrically on the bornologically bounded set `s` in a set `X`, then the image of `s` under scalar multiplication by any `c` in `G` is also bornologically bounded.
|
edist_mul_right
theorem edist_mul_right :
∀ {M : Type u} [inst : Mul M] [inst_1 : PseudoEMetricSpace M] [inst_2 : IsometricSMul Mᵐᵒᵖ M] (a b c : M),
edist (a * c) (b * c) = edist a b
This theorem, `edist_mul_right`, states that for any type `M` that has a multiplication operation, is a pseudo emetric space, and has a right-side isometric scalar multiplication, the distance (measured with the extended metric `edist`) between the results of multiplying two elements `a` and `b` by a third element `c` is equal to the distance between `a` and `b` themselves. In mathematical terms, for any `a`, `b`, and `c` in `M`, `edist (a * c) (b * c) = edist a b`.
More concisely: For any type `M` with a multiplication operation, a pseudo-metric `edist`, and right-isometric scalar multiplication, `edist (a * c) (b * c) = edist a b` for all `a, b, c` in `M`.
|
isometry_mul_right
theorem isometry_mul_right :
∀ {M : Type u} [inst : Mul M] [inst_1 : PseudoEMetricSpace M] [inst_2 : IsometricSMul Mᵐᵒᵖ M] (a : M),
Isometry fun x => x * a
The theorem `isometry_mul_right` states that for any given type `M`, if `M` has an operation of multiplication (`Mul`), has a structure of a pseudoemetric space (`PseudoEMetricSpace`), and scalar multiplication by elements of `Mᵐᵒᵖ` is an isometry (`IsometricSMul`), then for any element `a` of `M`, the function that multiplies every element of `M` by `a` from the right is an isometry. In other words, in such a space, right multiplication by a fixed element preserves the edistance between any two points.
More concisely: If `M` is a type equipped with a pseudo-metric, multiplication, and isometric right scalar multiplication, then right multiplication by any fixed element preserves the pseudo-metric.
|
dist_add_left
theorem dist_add_left :
∀ {M : Type u} [inst : PseudoMetricSpace M] [inst_1 : Add M] [inst_2 : IsometricVAdd M M] (a b c : M),
dist (a + b) (a + c) = dist b c
This theorem, referred to as `dist_add_left`, states that for any type `M` that is a pseudo metric space (a space where distances between points are defined and satisfy certain properties), and supports addition and isometric vector addition (meaning it has a "size" or "length" that is preserved under addition), the distance between the sum of `a` and `b` and the sum of `a` and `c` is equivalent to the distance between `b` and `c`. Simply put, it says that in such a space, adding the same element `a` to two different points `b` and `c` does not change the distance between those points.
More concisely: In a pseudo metric space with isometric vector addition, the distance between `a + b` and `a + c` is equal to the distance between `b` and `c`.
|
isometry_vadd
theorem isometry_vadd :
∀ {M : Type u} (X : Type w) [inst : PseudoEMetricSpace X] [inst_1 : VAdd M X] [inst_2 : IsometricVAdd M X] (c : M),
Isometry fun x => c +ᵥ x
The theorem `isometry_vadd` states that for any type `M`, any pseudometric space `X` and any vector addition operation `+ᵥ` which is isometric on `M` and `X`, given any element `c` of type `M`, the function that adds `c` to any element of `X` is an isometry. This means that adding `c` preserves the edistance between any two elements in the pseudometric space `X`.
More concisely: For any pseudometric space `(X, d)` and type `M` with an isometric vector addition `+ᵥ` on `M` and `X`, the function `x même c : X -> X` defined by `x meille c := x +ᵥ c` is an isometry.
|
edist_neg_neg
theorem edist_neg_neg :
∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsometricVAdd G G]
[inst_3 : IsometricVAdd Gᵃᵒᵖ G] (a b : G), edist (-a) (-b) = edist a b
This theorem, `edist_neg_neg`, states that for any type `G` which is an additive group and a pseudo-emetric space with isometric vector addition and such that its additive opposite (`Gᵃᵒᵖ`) also has isometric vector addition, the extended distance (denoted by `edist`) between the negations of two elements `a` and `b` of `G` is equal to the extended distance between `a` and `b` themselves. In other words, negating the elements doesn't change the distance between them.
More concisely: For any additive group `G` equipped with an isometric vector addition and having an isometric additive inverse such that the same properties hold for the additive opposite `Gᵃᵒᵖ`, the extended distance between the negations of two elements `a` and `b` is equal to the extended distance between `a` and `b` itself.
|
Metric.vadd_closedBall
theorem Metric.vadd_closedBall :
∀ {G : Type v} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : AddGroup G] [inst_2 : AddAction G X]
[inst_3 : IsometricVAdd G X] (c : G) (x : X) (r : ℝ), c +ᵥ Metric.closedBall x r = Metric.closedBall (c +ᵥ x) r
The theorem `Metric.vadd_closedBall` states that for any pseudometric space `X`, any additive group `G`, any action of `G` on `X`, and any isometric vector addition in `X`, for any elements `c` in `G`, `x` in `X`, and any real number `r`, the vector addition of `c` and the closed ball centered at `x` with radius `r` in `X` is equal to the closed ball in `X` centered at the vector addition of `c` and `x` with the same radius `r`. In other words, adding a vector to all points in a closed ball is equivalent to shifting the center of the ball by the same vector.
More concisely: For any pseudometric space X, additive group G acting on X, and isometric vector addition, the closed ball centered at x in X with radius r is equal to the closed ball centered at c × x in X with radius r, where c is an element of G.
|
dist_mul_left
theorem dist_mul_left :
∀ {M : Type u} [inst : PseudoMetricSpace M] [inst_1 : Mul M] [inst_2 : IsometricSMul M M] (a b c : M),
dist (a * b) (a * c) = dist b c
The theorem `dist_mul_left` states that for any type `M` that is a pseudo-metric space with multiplication and for which scalar multiplication is isometric, the distance between the product of two elements `a` and `b` and the product of the same `a` and another element `c` is the same as the distance between `b` and `c`. In other words, multiplying by `a` does not change the distance between `b` and `c`.
More concisely: For any pseudo-metric space `M` with multiplication and isometric scalar multiplication, the distance between `a * b` and `a * c` equals the distance between `b` and `c`.
|
isometry_smul
theorem isometry_smul :
∀ {M : Type u} (X : Type w) [inst : PseudoEMetricSpace X] [inst_1 : SMul M X] [inst_2 : IsometricSMul M X] (c : M),
Isometry fun x => c • x
This theorem states that, for any pseudoemetric space `X` and any type `M` with a scalar multiplication operation on `X` (denoted as `SMul M X`), if the scalar multiplication is isometric (i.e., it preserves the edistance, as captured by the `IsometricSMul M X` instance), then for any element `c` of type `M`, the function that multiplies each element of `X` by `c` is an isometry. In other words, scalar multiplication by `c` doesn't change the distances between the elements of the pseudoemetric space `X`.
More concisely: For any pseudometric space `X` and type `M` with an isometric scalar multiplication `SMul M X`, the function that multiplies each element of `X` by an element `c` of `M` is an isometry. In other words, the scalar multiplication preserves the pseudo-metric on `X`.
|
dist_add_right
theorem dist_add_right :
∀ {M : Type u} [inst : Add M] [inst_1 : PseudoMetricSpace M] [inst_2 : IsometricVAdd Mᵃᵒᵖ M] (a b c : M),
dist (a + c) (b + c) = dist a b
This theorem, `dist_add_right`, states that for any type `M` that has an addition operation, is a pseudo metric space, and has an isometric space over addition, the distance between the sum of `a` and `c` and the sum of `b` and `c` is equal to the distance between `a` and `b`. In other words, adding the same value `c` to both `a` and `b` does not change their distance in the metric space, denoting the property of translation invariance in the metric space.
More concisely: For any pseudo metric space `M` with an isometric space over addition, the distance between `a + c` and `b + c` equals the distance between `a` and `b` for all elements `a, b, c` in `M`.
|
edist_inv_inv
theorem edist_inv_inv :
∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsometricSMul G G]
[inst_3 : IsometricSMul Gᵐᵒᵖ G] (a b : G), edist a⁻¹ b⁻¹ = edist a b
This theorem states that for any type `G` that forms a Group and is a PseudoEMetricSpace, and under the conditions that scalar multiplication `IsometricSMul` is defined both for `G` and its opposite `Gᵐᵒᵖ`, the extended distance `edist` between the inverses `a⁻¹` and `b⁻¹` of any two elements `a` and `b` of `G` is equal to the extended distance between `a` and `b` themselves. This essentially means that in such a space, taking inverses doesn't affect the distance between elements.
More concisely: For any group `G` that is a PseudoEMetricSpace with isometric scalar multiplication, the extended distance between the inverses of any two elements is equal to the extended distance between the elements themselves.
|
Metric.vadd_ball
theorem Metric.vadd_ball :
∀ {G : Type v} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : AddGroup G] [inst_2 : AddAction G X]
[inst_3 : IsometricVAdd G X] (c : G) (x : X) (r : ℝ), c +ᵥ Metric.ball x r = Metric.ball (c +ᵥ x) r
The theorem `Metric.vadd_ball` states that for any pseudo metric space `X`, any add group `G`, any action of `G` on `X`, and any isometric additive action of `G` on `X`, given a group element `c`, a point `x` in `X`, and a real number `r`, the set obtained by adding `c` to every point in the open ball of radius `r` centered at `x` (`c +ᵥ Metric.ball x r`) is the same as the open ball of radius `r` centered at `c +ᵥ x` (`Metric.ball (c +ᵥ x) r`). In other words, it's the property of invariance of open balls under isometric additive actions.
More concisely: For any pseudo metric space, group, action, and isometric additive action, the open ball of radius r centered at x is equal to the set obtained by adding a group element c to every point in the open ball of radius r centered at x.
|
Bornology.IsBounded.vadd
theorem Bornology.IsBounded.vadd :
∀ {G : Type v} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : VAdd G X] [inst_2 : IsometricVAdd G X]
{s : Set X}, Bornology.IsBounded s → ∀ (c : G), Bornology.IsBounded (c +ᵥ s)
The theorem `Bornology.IsBounded.vadd` states that given an additive isometric action of a type `G` on a type `X`, where `X` is a pseudo metric space and `G` is equipped with an operation of vector addition and this operation is isometric, if a set `s` in `X` is bounded with respect to the ambient bornology on `X`, then the image of the set `s` under translation by any element `c` from `G` is also bounded. In other words, a bounded set remains bounded under an isometric additive action.
More concisely: If `s` is a bounded subset of a pseudo metric space `X` with respect to its bornology, and `G` is an additive isometric group of transformations on `X`, then for all `c` in `G`, the translated set `c.map s` is also bounded.
|
edist_vadd_left
theorem edist_vadd_left :
∀ {M : Type u} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : VAdd M X] [inst_2 : IsometricVAdd M X] (c : M)
(x y : X), edist (c +ᵥ x) (c +ᵥ y) = edist x y
This theorem, named `edist_vadd_left`, states that for any types `M` and `X`, given that `X` forms a pseudoemetric space and that `M` can be vector added to `X` in an isometric fashion (i.e., preserving the distance), the distance from `c +ᵥ x` to `c +ᵥ y` (where `c` is in `M`, `x` and `y` are in `X`) is the same as the distance from `x` to `y`. In mathematical notation, this is saying that for all `c`, `x`, `y`, we have `edist (c +ᵥ x) (c +ᵥ y) = edist x y`, where `edist` represents the extended distance function in the pseudoemetric space.
More concisely: For any pseudometric space `(X, edist)` and vector `c` in a vector space `M` that can be isometrically added to `X`, the extended distance `edist` between `c +ᵥ x` and `c +ᵥ y` equals the extended distance between `x` and `y`, for all `x, y` in `X`.
|
isometry_add_right
theorem isometry_add_right :
∀ {M : Type u} [inst : Add M] [inst_1 : PseudoEMetricSpace M] [inst_2 : IsometricVAdd Mᵃᵒᵖ M] (a : M),
Isometry fun x => x + a
This theorem states that for any type `M` that has an addition operation, is a pseudoemetric space, and satisfies the property of being an isometric vector addition space on the opposite side (`Mᵃᵒᵖ`), for any element `a` of `M`, the transformation that adds `a` to every element in the space is an isometry. In other words, adding a fixed value to every point in the space preserves the pseudoemetric (the "distance" between two points in the space), i.e., the distance between any two points remains unchanged when the same value is added to both of them.
More concisely: For any isometric vector addition space `M` with pseudometric `d` and element `a`, the translation function `x ↦ x + a` is an isometry with respect to `d`.
|