Isometry.continuous
theorem Isometry.continuous :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
Isometry f → Continuous f
This theorem states that an isometry is continuous. More specifically, for any two types `α` and `β` that are pseudoemetric spaces, if `f` is a function mapping from `α` to `β` and `f` is an isometry (i.e., it preserves the extended distance between any two points in `α`), then `f` is also a continuous function. This is a fundamental theorem in topology and metric spaces, showing the continuity of distance-preserving transformations.
More concisely: If `f` is an isometry between pseudometric spaces `α` and `β`, then `f` is a continuous function.
|
IsometryEquiv.image_closedBall
theorem IsometryEquiv.image_closedBall :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (h : α ≃ᵢ β) (x : α)
(r : ℝ), ⇑h '' Metric.closedBall x r = Metric.closedBall (h x) r
The theorem `IsometryEquiv.image_closedBall` states that for any isometry `h` between two pseudo metric spaces `α` and `β`, the image of the closed ball in `α` centered at `x` with radius `r` under the isometry `h` is the closed ball in `β` centered at `h(x)` with the same radius `r`. In other words, an isometry maps a closed ball in one pseudo metric space to a closed ball with the same radius in the other pseudo metric space.
More concisely: For any isometry between pseudo metric spaces and any point and radius in those spaces, the image of the closed ball centered at that point with that radius is a closed ball with the same radius centered at the image of that point in the other space.
|
Isometry.prod_map
theorem Isometry.prod_map :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
[inst_2 : PseudoEMetricSpace γ] {δ : Type u_2} [inst_3 : PseudoEMetricSpace δ] {f : α → β} {g : γ → δ},
Isometry f → Isometry g → Isometry (Prod.map f g)
The theorem `Isometry.prod_map` states that for any two given isometric mappings `f` and `g` - where `f` is a map from a pseudoemetric space `α` to another pseudoemetric space `β`, and `g` is a map from a pseudoemetric space `γ` to another pseudoemetric space `δ` - the function `Prod.map f g` is also an isometry. In other words, if `f` and `g` preserve the pseudoemetric distance between elements of their respective domains, then the function that applies `f` to the first component of a pair and `g` to the second also preserves the pseudoemetric distance.
More concisely: If `f` is an isometry from pseudometric space `α` to `β` and `g` is an isometry from pseudometric space `γ` to `δ`, then the function `Prod.map f g : α × γ → β × δ` is an isometry.
|
Isometry.of_nndist_eq
theorem Isometry.of_nndist_eq :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
(∀ (x y : α), nndist (f x) (f y) = nndist x y) → Isometry f
The theorem `Isometry.of_nndist_eq` states that for any two types `α` and `β`, each equipped with a pseudometric space structure, and for any function `f` from `α` to `β`, if `f` preserves the non-negative distance (denoted by `nndist`) between every pair of points in `α` (that is, the non-negative distance between `f(x)` and `f(y)` is always equal to the non-negative distance between `x` and `y`), then `f` is an isometry. In other words, `f` preserves the edistance (extended distance) between every pair of points.
More concisely: If a function between two pseudometric spaces preserves the non-negative distance between all pairs of points, then it is an isometry.
|
Isometry.diam_range
theorem Isometry.diam_range :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
Isometry f → Metric.diam (Set.range f) = Metric.diam Set.univ
The theorem `Isometry.diam_range` states that for any two types `α` and `β` that are pseudo metric spaces, and for any function `f` from `α` to `β`, if `f` is an isometry (a map that preserves the pseudo metric), then the diameter of the range of `f` is equal to the diameter of the universal set `α`. In other words, an isometric function does not change the diameter of the space.
More concisely: For any pseudo metric spaces α and β and isometric function f from α to β, the diameter of the range of f equals the diameter of α.
|
UniformEmbedding.to_isometry
theorem UniformEmbedding.to_isometry :
∀ {α : Type u_2} {β : Type u_3} [inst : UniformSpace α] [inst_1 : MetricSpace β] {f : α → β}
(h : UniformEmbedding f), Isometry f
The theorem `UniformEmbedding.to_isometry` states that for any function `f` from a type `α` in a uniform space to a type `β` in a metric space, if `f` is a uniform embedding (which preserves the uniformity structure), then `f` is also an isometry. This means that `f` preserves the distances between the elements in the source space `α` when embedded in the target space `β`, specifically, the distance (`edist`) between any two points `x1` and `x2` in `α` is equal to the distance between `f(x1)` and `f(x2)` in `β`.
More concisely: If `f : α → β` is a uniform embedding from the uniform space `(α, δ)` to the metric space `(β, d)`, then `f` is an isometry, that is, `δ(x₁, x₂) = d(f(x₁), f(x₂))` for all `x₁, x₂ ∈ α`.
|
IsometryEquiv.apply_symm_apply
theorem IsometryEquiv.apply_symm_apply :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β) (y : β),
h (h.symm y) = y
The theorem `IsometryEquiv.apply_symm_apply` states that for any two types `α` and `β` which are both `PseudoEMetricSpace`s, for any isometric isomorphism `h` from `α` to `β`, and for any element `y` of type `β`, applying the isomorphism `h` to the result of applying the inverse of `h` (obtained through `IsometryEquiv.symm`) to `y` will yield `y` itself. In other words, it states that the isomorphism and its inverse are indeed inverse operations to each other in the context of isometric isomorphisms between two pseudo-emetric spaces.
More concisely: For any isometric isomorphism between two pseudo-metric spaces and any element in the image space, applying the isomorphism followed by its symmetric inverse yields the original element.
|
Isometry.injective
theorem Isometry.injective :
∀ {α : Type u} {β : Type v} [inst : EMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
Isometry f → Function.Injective f
This theorem states that if a function `f` from one emetric space `α` to another emetric space or pseudoemetric space `β` is an isometry, meaning it preserves the extended distance (`edist`) between any two points in `α`, then `f` is also injective. In other words, if `f(x)` equals `f(y)`, it must be the case that `x` equals `y`. This is a fundamental property of isometric embeddings in metric and pseudoemetric spaces.
More concisely: If `f: α → β` is an isometry between metric or pseudometric spaces `α` and `β`, then `f` is injective.
|
IsometryEquiv.image_symm
theorem IsometryEquiv.image_symm :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β),
Set.image ⇑h.symm = Set.preimage ⇑h
The theorem `IsometryEquiv.image_symm` states that for any isometric isomorphism `h` from a pseudo-emetric space `α` to another pseudo-emetric space `β`, the image of a set under the inverse of `h` is equivalent to the preimage of the set under `h`. In other words, when we apply `h` to elements of `α`, and take the image through the inverse of `h`, we end up with the same set as if we started with `β` and considered all elements that map to it under `h`.
More concisely: For any isometric isomorphism between pseudo-metric spaces, the image of a set under the inverse mapping is equivalent to the preimage of that set.
|
Isometry.comp_continuous_iff
theorem Isometry.comp_continuous_iff :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β} {γ : Type u_2}
[inst_2 : TopologicalSpace γ], Isometry f → ∀ {g : γ → α}, Continuous (f ∘ g) ↔ Continuous g
The theorem `Isometry.comp_continuous_iff` states that for any types `α`, `β`, and `γ`, where `α` and `β` are pseudoemetric spaces and `γ` is a topological space, for any function `f` from `α` to `β`, if `f` is an isometry, then for any function `g` from `γ` to `α`, the composition of `f` and `g` is continuous if and only if `g` is continuous. This means that the continuity of the composition function `f ∘ g` is solely determined by the continuity of `g` when `f` is an isometry.
More concisely: For any pseudometric spaces α, β, and topological space γ, if f : α → β is an isometry and g : γ → α is continuous, then their composition f ∘ g is also continuous. Conversely, if f : α → β is an isometry, then f ∘ g is continuous if and only if g is continuous.
|
IsometryEquiv.range_eq_univ
theorem IsometryEquiv.range_eq_univ :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β),
Set.range ⇑h = Set.univ
This theorem states that for any two types `α` and `β` equipped with `PseudoEMetricSpace` structures, if there is an isometry (denoted as `α ≃ᵢ β`), then the range of this isometric equivalence maps to the universal set of `β`. In other words, the isometry is surjective, mapping every element of `α` to some element in `β`.
More concisely: Given types `α` and `β` with `PseudoEMetricSpace` structures and an isometry `α ≃ᵢ β`, every element in `α` is mapped to some element in `β`.
|
Mathlib.Topology.MetricSpace.Isometry._auxLemma.1
theorem Mathlib.Topology.MetricSpace.Isometry._auxLemma.1 : ∀ {p q : NNReal}, (↑p = ↑q) = (p = q)
This theorem states that for any two nonnegative real numbers 'p' and 'q', the equality of their embeddings (that is, considering 'p' and 'q' as real numbers rather than as nonnegative real numbers) is equivalent to the equality of 'p' and 'q' themselves. In other words, two nonnegative real numbers 'p' and 'q' are equal if and only if their corresponding real numbers are equal.
More concisely: For any nonnegative real numbers p and q, p = q if and only if their corresponding real numbers are equal.
|
Isometry.preimage_ball
theorem Isometry.preimage_ball :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
Isometry f → ∀ (x : α) (r : ℝ), f ⁻¹' Metric.ball (f x) r = Metric.ball x r
This theorem states that for any two pseudo-metric spaces `α` and `β`, and any function `f` from `α` to `β` that is an isometry, the pre-image under `f` of the open ball in `β` centered at `f(x)` with radius `r` is exactly the open ball in `α` centered at `x` with the same radius `r`. In other words, if you take a point `x` in `α` and consider the open ball around `x` in `α`, then apply the isometry `f` which maps this ball to a ball in `β`, if you then take the inverse image of this latter ball under `f`, you end up with the original ball in `α`. This is a consequence of the defining property of isometries that they preserve distances.
More concisely: For any isometry `f` between pseudo-metric spaces `α` and `β` and any point `x` in `α`, the pre-image under `f` of the open ball in `β` centered at `f(x)` with radius `r` is the open ball in `α` centered at `x` with radius `r`.
|
IsometryEquiv.image_ball
theorem IsometryEquiv.image_ball :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (h : α ≃ᵢ β) (x : α)
(r : ℝ), ⇑h '' Metric.ball x r = Metric.ball (h x) r
This theorem states that for every pseudometric spaces `α` and `β`, every isometry `h` from `α` to `β`, every point `x` in `α`, and every real number `r`, the image of the open ball of radius `r` centered at `x` under the isometry `h` is exactly the open ball of radius `r` centered at `h(x)`. In other words, an isometry preserves open balls: it takes every point inside an open ball around `x` in `α` to a point inside the corresponding open ball around `h(x)` in `β`, and vice versa.
More concisely: For every isometry between pseudometric spaces and every point and radius in those spaces, the image of the open ball centered at under is the open ball centered at in with the same radius.
|
Isometry.of_dist_eq
theorem Isometry.of_dist_eq :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
(∀ (x y : α), dist (f x) (f y) = dist x y) → Isometry f
The theorem `Isometry.of_dist_eq` states that for any types `α` and `β` which are pseudometric spaces, a function `f` from `α` to `β` is an isometry if it preserves the distances between all points `x` and `y` in `α`. In other words, if for every pair of elements `(x, y)` in `α`, the distance between `f(x)` and `f(y)` in `β` is equal to the distance between `x` and `y` in `α`, then `f` is an isometry.
More concisely: If `f: α → β` preserves the distances between all pairs of points in pseudometric spaces `α` and `β`, then `f` is an isometry.
|
IsometryEquiv.dist_eq
theorem IsometryEquiv.dist_eq :
∀ {α : Type u_2} {β : Type u_3} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (h : α ≃ᵢ β) (x y : α),
dist (h x) (h y) = dist x y
This is a theorem about isometries in the context of pseudo metric spaces. The theorem states that for any two types `α` and `β`, both equipped with a pseudo metric space structure, if there is an isometric equivalence `h` from `α` to `β`, then for any two elements `x` and `y` of `α`, the distance between the images of `x` and `y` under `h` in `β`, is the same as the distance between `x` and `y` in `α`. In other words, an isometry preserves distances between points.
More concisely: Given isometric equivalences between pseudo metric spaces `α` and `β`, the distance between images of any two points `x` and `y` in `α` equals the distance between these points in `β`.
|
Isometry.preimage_sphere
theorem Isometry.preimage_sphere :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
Isometry f → ∀ (x : α) (r : ℝ), f ⁻¹' Metric.sphere (f x) r = Metric.sphere x r
This theorem states that for any types `α` and `β` which have a pseudo-metric space structure, any function `f` from `α` to `β`, if `f` is an isometry (meaning it preserves the distance between any two elements in `α`), then the preimage of the sphere centered at `f(x)` with radius `r` under `f` is equal to the sphere centered at `x` with radius `r` in `α`. In other words, the isometrically transformed points from the sphere in the domain space `α` form a sphere with the same radius in the codomain space `β`.
More concisely: For any isometric function `f` between pseudo-metric spaces `(α, dα)` and `(β, dβ)`, the preimage of the sphere `{y ∈ β : dβ(y, f(x)) = r}` centered at `f(x)` with radius `r` is equal to the sphere `{x ∈ α : dα(x, x') = r}`, where `x'` is any point in `α` with `dα(x, x') = r`.
|
Isometry.preimage_closedBall
theorem Isometry.preimage_closedBall :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
Isometry f → ∀ (x : α) (r : ℝ), f ⁻¹' Metric.closedBall (f x) r = Metric.closedBall x r
The theorem `Isometry.preimage_closedBall` states that for any isometry `f` between two pseudometric spaces `α` and `β`, for any point `x` in `α` and any real number `r`, the preimage of the closed ball centered at `f(x)` with radius `r` under `f` is exactly the closed ball centered at `x` with radius `r`. In other words, an isometry maps closed balls in the domain space to corresponding closed balls in the codomain space, preserving their centers and radii.
More concisely: For any isometry between pseudometric spaces and any point and radius, the preimage of the closed ball centered at the image point with the given radius is the closed ball centered at the original point with the same radius.
|
Isometry.embedding
theorem Isometry.embedding :
∀ {α : Type u} {β : Type v} [inst : EMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
Isometry f → Embedding f
The theorem states that for any types `α` and `β`, where `α` is an extended metric space and `β` is a pseudo-extended metric space, if `f` is a function mapping from `α` to `β` and `f` is an isometry (meaning it preserves the extended distance between any two points in `α` when mapped to `β`), then `f` is also an embedding. In the context of metric spaces, an embedding is a function that preserves the structure of the space, meaning that it is injective and the topology of the image is the same as the topology of the original space.
More concisely: Given types `α` with `α` an extended metric space and `β` a pseudo-extended metric space, if `f: α → β` is an isometry (distance-preserving function), then it is an embedding (injective function preserving the topology).
|
Isometry.closedEmbedding
theorem Isometry.closedEmbedding :
∀ {α : Type u} {γ : Type w} [inst : EMetricSpace α] [inst_1 : CompleteSpace α] [inst_2 : EMetricSpace γ]
{f : α → γ}, Isometry f → ClosedEmbedding f
This theorem states that if you have an isometry, which is a function that preserves the extended distance (edist) between any two points in a pseudometric space, from a complete extended metric (emetric) space to any other emetric space, then this isometry is a closed embedding. In other words, if a function maps from a space where every Cauchy sequence converges to a limit to another space while preserving distances, then that function has the property that the image of a closed set under this function is also closed.
More concisely: If f is an isometry between complete extended metric spaces, then the image of a closed set under f is closed.
|
isometry_subtype_coe
theorem isometry_subtype_coe : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α}, Isometry Subtype.val := by
sorry
The theorem `isometry_subtype_coe` states that for any type `α` which has the structure of a PseudoEMetricSpace and any set `s` of elements from `α`, the function `Subtype.val` is an isometry. In other words, when we have a subtype defined by some property on elements of `α` (i.e., a set of particular elements from `α`), the function that simply returns the underlying element of the subtype (ignoring the property that defines the subtype) preserves the pseudometric space structure. This means it does not change the edistance (extended distance) between any pair of points.
More concisely: For any PseudoEMetricSpace `α` and subset `s` of `α`, the function `Subtype.val : s → α` is an isometry regarding the pseudometric.
|
Isometry.ediam_image
theorem Isometry.ediam_image :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
Isometry f → ∀ (s : Set α), EMetric.diam (f '' s) = EMetric.diam s
This theorem states that isometries, which are functions preserving the extended distance between elements in pseudoemetric spaces, also preserve the diameter of a set in such spaces. More specifically, for every type `α` and `β` with a pseudoemetric space structure, for every isometric function `f` from `α` to `β`, and for any set `s` of type `α`, the diameter of the image of `s` under `f` is equal to the diameter of `s` itself.
More concisely: Given a pseudometric space `(α, d)` and an isometric function `f: α → β` between pseudometric spaces `(α, d)` and `(β, δ)`, the diameter of `f(S)` equals the diameter of `S` for any set `S ⊆ α`.
|
IsometryEquiv.isometry
theorem IsometryEquiv.isometry :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β),
Isometry ⇑h
The theorem `IsometryEquiv.isometry` states that for any two pseudoemetric spaces, `α` and `β`, if there is an isometric equivalence `h` between them, then the function represented by `h` is an isometry. In other words, the function `h` preserves the edistance between any two points in `α` when mapping them into `β`. This means that for any two points `x1` and `x2` in `α`, the edistance between `f(x1)` and `f(x2)` in `β` is the same as the edistance between `x1` and `x2` in `α`.
More concisely: If `h` is an isometric equivalence between pseudometric spaces `α` and `β`, then `h` is an isometry, that is, for all `x₁, x₂` in `α`, the edistances `edist α x₁ x₂` and `edist β (h x₁) (h x₂)` are equal.
|
isometry_dcomp
theorem isometry_dcomp :
∀ {ι : Type u_4} [inst : Fintype ι] {α : ι → Type u_2} {β : ι → Type u_3}
[inst_1 : (i : ι) → PseudoEMetricSpace (α i)] [inst_2 : (i : ι) → PseudoEMetricSpace (β i)]
(f : (i : ι) → α i → β i), (∀ (i : ι), Isometry (f i)) → Isometry fun g i => f i (g i)
This theorem, `isometry_dcomp`, states that for any finite index set `ι` and any indexed families of types `α` and `β` (indexed by `ι`), where each `α i` and `β i` is a pseudoemetric space, if for each index `i` there is an isometry from `α i` to `β i` (denoted as `f i : α i → β i`), then the function that takes a function `g : ι → α i` and an index `i` and returns `f i (g i)` is also an isometry. In other words, if each `f i` preserves the pseudoemetric distance, then the composite function `fun g i => f i (g i)` also preserves the pseudoemetric distance.
More concisely: Given a finite index set `ι` and indexed families of pseudometric spaces `α` and `β` with isometries `f i : α i ↔ β i` for each index `i`, the function that maps `g : ι → α i` to `f i (g i)` is an isometry between `α` and `β`.
|
isometry_iff_dist_eq
theorem isometry_iff_dist_eq :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
Isometry f ↔ ∀ (x y : α), dist (f x) (f y) = dist x y
This theorem states that, in the context of pseudometric spaces, a function is an isometry (i.e., a map that preserves distances) if and only if the distance between the images of any two points under this function is equal to the distance between the points themselves. In other words, for any pseudometric spaces `α` and `β` and any function `f` from `α` to `β`, `f` is an isometry if for every pair of points `x` and `y` in `α`, the distance between `f(x)` and `f(y)` in `β` is the same as the distance between `x` and `y` in `α`.
More concisely: A function between two pseudometric spaces is an isometry if and only if the distance between its images of any two points is equal to the distance between the points themselves.
|
isometry_id
theorem isometry_id : ∀ {α : Type u} [inst : PseudoEMetricSpace α], Isometry id
This theorem states that the identity function is an isometry in any pseudoemetric space. In other words, for all points in a pseudoemetric space, the edistance (extended distance) between any two points remains the same after applying the identity function. In mathematical terms, for a pseudoemetric space $\alpha$ and any two points $x_1, x_2$ in this space, the edistance after applying the identity is the same as the original edistance, i.e., $\text{edist}(\text{id}(x_1), \text{id}(x_2)) = \text{edist}(x_1, x_2)$.
More concisely: In any pseudometric space, the identity function preserves the extended distance, that is, for all points x₁, x₂, edist(id(x₁), id(x₂)) = edist(x₁, x₂).
|
IsometryEquiv.preimage_ball
theorem IsometryEquiv.preimage_ball :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (h : α ≃ᵢ β) (x : β)
(r : ℝ), ⇑h ⁻¹' Metric.ball x r = Metric.ball (h.symm x) r
The theorem `IsometryEquiv.preimage_ball` states that for any isometric isomorphism `h` between two pseudo metric spaces `α` and `β`, any point `x` in `β`, and any real number `r`, the pre-image under `h` of the open ball of radius `r` centered at `x` is equal to the open ball of radius `r` centered at the point in `α` that corresponds to `x` under the inverse of `h`. In other words, an isometric isomorphism preserves the concept of open balls under pre-image mapping.
More concisely: For any isometric isomorphism between pseudo metric spaces and any point and radius in the target space, the preimage under the isomorphism of the open ball centered at that point is the open ball centered at the preimage point in the source space.
|
Mathlib.Topology.MetricSpace.Isometry._auxLemma.2
theorem Mathlib.Topology.MetricSpace.Isometry._auxLemma.2 :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
Isometry f = ∀ (x y : α), nndist (f x) (f y) = nndist x y
The theorem `Mathlib.Topology.MetricSpace.Isometry._auxLemma.2` in natural language states: For all types `α` and `β` that are instances of `PseudoMetricSpace`, and for any function `f` from `α` to `β`, `f` is an isometry (a map preserving the extended distance between pseudoemetric spaces) if and only if for all `x` and `y` in `α`, the non-negative distance (nndist) between `f(x)` and `f(y)` in `β` is equal to the non-negative distance between `x` and `y` in `α`.
More concisely: A function between two pseudo-metric spaces is an isometry if and only if it preserves non-negative distances, i.e., the distance between the images of any two points is equal to the distance between the points themselves.
|
Isometry.right_inv
theorem Isometry.right_inv :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β} {g : β → α},
Isometry f → Function.RightInverse g f → Isometry g
The theorem states that the right inverse of an isometry is also an isometry. In more detail, given two types `α` and `β` which are pseudoemetric spaces and functions `f : α → β` and `g : β → α`, if `f` is an isometry (meaning it preserves the edistance between any two points) and `g` is a right inverse to `f` (meaning the composition `f ∘ g` equals the identity function), then `g` is also an isometry.
More concisely: If a function is an isometry and has a right inverse, then the right inverse is also an isometry.
|
Isometry.preimage_setOf_dist
theorem Isometry.preimage_setOf_dist :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
Isometry f → ∀ (x : α) (p : ℝ → Prop), f ⁻¹' {y | p (dist y (f x))} = {y | p (dist y x)}
The theorem `Isometry.preimage_setOf_dist` states that for all types `α` and `β` that are instances of PseudoMetricSpace, for all functions `f` from `α` to `β` that are isometries, and for all `x` in `α` and predicate `p` on real numbers, the preimage of the set of elements in `β` that satisfy predicate `p` with the distance to `f(x)` under the function `f` is exactly the set of elements in `α` that satisfy predicate `p` with the distance to `x`. In simpler terms, this means that an isometry `f` preserves the property of distance: the set of points in `α` that have a certain property with respect to their distance to `x` is mapped by `f` onto the set of points in `β` that have the same property with respect to their distance to `f(x)`.
More concisely: For any isometry between PseudoMetricSpaces, the preimages of sets defined by distance conditions are equal under the isometry.
|
Isometry.antilipschitz
theorem Isometry.antilipschitz :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
Isometry f → AntilipschitzWith 1 f
The theorem `Isometry.antilipschitz` states that for any two types `α` and `β` that are pseudo e-metric spaces, if a function `f` from `α` to `β` is an isometry (which by definition means it preserves the e-distance between any two points from `α`), then `f` is `AntilipschitzWith` a constant `K` equal to 1. In other words, for any two points in `α`, the e-distance between these two points is always less than or equal to 1 times the e-distance between their images under `f`.
More concisely: Given isometric functions between pseudometric spaces, the function is antilipschitz with constant 1.
|
IsometryEquiv.image_sphere
theorem IsometryEquiv.image_sphere :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (h : α ≃ᵢ β) (x : α)
(r : ℝ), ⇑h '' Metric.sphere x r = Metric.sphere (h x) r
The theorem `IsometryEquiv.image_sphere` states that for any two types `α` and `β` that have the structure of a pseudometric space, and for any isometry `h` from `α` to `β`, the image under `h` of the sphere of radius `r` centered at a point `x` in `α` is precisely the sphere of the same radius `r` centered at the image of `x` under `h` in `β`. In other words, an isometry maps spheres to spheres of the same radius, preserving their geometric structure.
More concisely: For any isometry between pseudometric spaces and any point and radius, the image of a sphere is a sphere of the same radius with the same center in the target space.
|
IsometryEquiv.symm_symm
theorem IsometryEquiv.symm_symm :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β),
h.symm.symm = h
This theorem states that for any two types `α` and `β` which have `PseudoEMetricSpace` structures, and given an isometric isomorphism `h` from `α` to `β`, applying the operation `IsometryEquiv.symm` twice (i.e., taking the inverse of the inverse) returns the original isometric isomorphism `h`. In other words, the `IsometryEquiv.symm` operation is its own inverse when applied twice.
More concisely: For any isometric isomorphism `h` between PseudoMetricSpaces `α` and `β`, `h` is equal to its own inverse, i.e., `h = IsometryEquiv.symm (IsometryEquiv.symm h)`.
|
Isometry.uniformContinuous
theorem Isometry.uniformContinuous :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
Isometry f → UniformContinuous f
This theorem states that an isometry from one pseudometric space to another is uniformly continuous. In other words, if a function `f` is an isometry, preserving the distance between all pairs of points in a pseudometric space `α`, then `f` is uniformly continuous. This means that if any two points `x` and `y` in `α` are close together, then their images `f(x)` and `f(y)` in the pseudometric space `β` are also close together, regardless of the specific location of `x` and `y` in the space `α`. The theorem generalizes this property to all functions that are isometries between any two pseudometric spaces.
More concisely: An isometry between two pseudometric spaces is a uniformly continuous function.
|
IsometryEquiv.continuous
theorem IsometryEquiv.continuous :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β),
Continuous ⇑h
This theorem states that for any two types `α` and `β`, which are pseudo emetric spaces (i.e., spaces equipped with a notion of distance that may take the value +∞), any isometric equivalence `h` between these spaces is continuous. In other words, if there is an isometry (a distance-preserving transformation) that forms a bijective correspondence between the elements of the two spaces, then this transformation is continuous, meaning that nearby points in the original space get mapped to nearby points in the target space.
More concisely: Given two pseudo metric spaces `α` and `β`, any isometric embedding `h : α → β` is a continuous function.
|
Isometry.dist_eq
theorem Isometry.dist_eq :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
Isometry f → ∀ (x y : α), dist (f x) (f y) = dist x y
The theorem `Isometry.dist_eq` states that for any two types `α` and `β` that are both instances of the `PseudoMetricSpace` type class, for any function `f` from `α` to `β`, if `f` is an isometry (i.e., a function that preserves the extended distance between elements in `α` and `β`), then for any two elements `x` and `y` in `α`, the distance between `f(x)` and `f(y)` in `β` is the same as the distance between `x` and `y` in `α`. In simple terms, an isometric function preserves the distances between elements under transformation.
More concisely: For any functions `f` between pseudo-metric spaces `α` and `β` that are isometries, `∋ x, y in α, dβ(f(x), f(y)) = dα(x, y)`, where `dα` and `dβ` denote the distance functions on `α` and `β`, respectively.
|
IsometryEquiv.ext
theorem IsometryEquiv.ext :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] ⦃h₁ h₂ : α ≃ᵢ β⦄,
(∀ (x : α), h₁ x = h₂ x) → h₁ = h₂
This theorem states that for any two isometries `h₁` and `h₂` from a pseudo emetric space `α` to another pseudo emetric space `β`, if for all elements `x` in `α` the images under `h₁` and `h₂` are equal (i.e., `h₁ x = h₂ x`), then `h₁` and `h₂` are the same isometry. In other words, two isometries between the same pseudo emetric spaces are equal if they map each point in the domain to the same point in the codomain.
More concisely: If two isometries between the same pseudo-metric spaces map each point to the same image, then they are equal.
|
isometry_iff_nndist_eq
theorem isometry_iff_nndist_eq :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
Isometry f ↔ ∀ (x y : α), nndist (f x) (f y) = nndist x y
This theorem states that in the context of pseudometric spaces, a function is an isometry if and only if it preserves nonnegative distances. In other words, for any two points in the domain of the function, the nonnegative distance between their images under the function is equal to the nonnegative distance between the points themselves. Here, pseudometric spaces are a generalization of metric spaces, where the distance between two distinct points can be zero. The nonnegative distance (nndist) is a variant of the distance function (dist) that guarantees a nonnegative real number as output.
More concisely: A function between pseudometric spaces is an isometry if and only if it preserves non-negative distances, i.e., nndist(x, y) = nndist(f(x), f(y)) for all x, y in the domain of f.
|
Isometry.nndist_eq
theorem Isometry.nndist_eq :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
Isometry f → ∀ (x y : α), nndist (f x) (f y) = nndist x y
The theorem `Isometry.nndist_eq` states that an isometry preserves non-negative distances. More formally, for any types `α` and `β` that are pseudo metric spaces, if `f` is an isometry, then for any elements `x` and `y` of type `α`, the non-negative distance `nndist` between the images `f x` and `f y` in `β` is equal to the original non-negative distance between `x` and `y` in `α`.
More concisely: An isometry preserves non-negative distances between elements in pseudo metric spaces, i.e., `nndist(f x, f y) = nndist(x, y)` for any isometry `f` and elements `x` and `y` in pseudo metric spaces `α` and `β`, respectively.
|
Isometry.edist_eq
theorem Isometry.edist_eq :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
Isometry f → ∀ (x y : α), edist (f x) (f y) = edist x y
This theorem states that an isometry function, in the context of two pseudoemetric spaces, preserves the extended distance (or "edistance") between any two points. More formally, given any pseudoemetric spaces 'α' and 'β', and any function 'f' from 'α' to 'β' that is an isometry, for any two points 'x' and 'y' in 'α', the edistance between the images of 'x' and 'y' under 'f' is equal to the edistance between 'x' and 'y'.
This means that the 'f' does not alter the edistance between any two points in the space which it maps - a property characteristic of isometry functions.
More concisely: Given any isometry function between two pseudometric spaces, the edistance between the images of any two points under the function is equal to the edistance between the original points.
|
IsometryEquiv.preimage_closedBall
theorem IsometryEquiv.preimage_closedBall :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (h : α ≃ᵢ β) (x : β)
(r : ℝ), ⇑h ⁻¹' Metric.closedBall x r = Metric.closedBall (h.symm x) r
The theorem `IsometryEquiv.preimage_closedBall` states that for any isometric isomorphism `h` between two pseudometric spaces `α` and `β`, the preimage of a closed ball in `β` centered at a point `x` with radius `r` under the isomorphism `h` is equal to the closed ball in `α` centered at the image of `x` under the inverse of the isomorphism `h` with the same radius `r`. In other words, applying an isometric isomorphism doesn't change the size of the closed ball, it simply relocates it.
More concisely: Given an isometric isomorphism between two pseudometric spaces and a point with radius in those spaces, the preimage of the closed ball centered at that point in the second space is equal to the closed ball centered at the image of that point in the first space under the inverse isomorphism.
|
Isometry.uniformInducing
theorem Isometry.uniformInducing :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
Isometry f → UniformInducing f
This theorem states that an isometry, which is a function that preserves the edistance (extended distance) between two elements in pseudoemetric spaces, from a particular pseudoemetric space, induces a uniform structure on that space. More precisely, for any two types `α` and `β` that are instances of `PseudoEMetricSpace`, and any function `f` from `α` to `β`, if `f` is an isometry, then `f` is also a uniform inducing map. A uniform inducing map is one that pulls back the uniform structure of the target space to the source space, essentially creating a uniformity on the source space that is compatible with the function.
More concisely: If `f` is an isometry between pseudometric spaces `α` and `β`, then `f` induces a uniform structure on `α` that is compatible with the source space's pseudometric and the uniform structure of `β`.
|
Isometry.ediam_range
theorem Isometry.ediam_range :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
Isometry f → EMetric.diam (Set.range f) = EMetric.diam Set.univ
The theorem `Isometry.ediam_range` states that for any two pseudoemetric spaces `α` and `β`, and a function `f` from `α` to `β`, if `f` is an isometry (a map preserving the extended distance between pseudoemetric spaces), then the diameter of the set of all outputs of `f` (`Set.range f`) is equal to the diameter of the universal set on `α` (`Set.univ`). This means that an isometric function preserves the diameter of the space in which it operates.
More concisely: For any isometry `f` between pseudometric spaces `α` and `β`, the diameter of `Set.range f` equals the diameter of `Set.univ α`.
|
Embedding.to_isometry
theorem Embedding.to_isometry :
∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : MetricSpace β] {f : α → β} (h : Embedding f),
Isometry f
This theorem states that for any two types `α` and `β`, where `α` is a topological space and `β` is a metric space, if there is a function `f` that embeds `α` into `β` (i.e., `f` is an embedding), then `f` preserves the distance between the elements of `α` when they are mapped to `β`, thereby making `f` an isometry. This is to say, the distance between any two points in `α` is the same as the distance between their images in `β` under `f`.
More concisely: If `α` is a topological space and `β` is a metric space with an embedding `f: α → β`, then `f` is an isometry, i.e., `d(x, y) = d(f(x), f(y))` for all `x, y ∈ α`, where `d` denotes the distance functions on `α` and `β`.
|
Isometry.lipschitz
theorem Isometry.lipschitz :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
Isometry f → LipschitzWith 1 f
The theorem `Isometry.lipschitz` states that for any two pseudoemetric spaces `α` and `β`, if a function `f` from `α` to `β` is an isometry (meaning that it preserves the extended distance between any two points from the domain), then `f` is Lipschitz continuous with the constant 1. In other words, for all points `x` and `y` in the domain, the extended distance between `f(x)` and `f(y)` is less than or equal to the extended distance between `x` and `y`.
More concisely: If `f` is an isometry between pseudometric spaces `α` and `β`, then `f` is Lipschitz continuous with constant 1.
|
isometry_subsingleton
theorem isometry_subsingleton :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β}
[inst_2 : Subsingleton α], Isometry f
The theorem `isometry_subsingleton` states that for any types `α` and `β` that are both `PseudoEMetricSpaces` (spaces equipped with a distance function that satisfies the properties of a pseudometric), any function `f` from `α` to `β` is an isometry (a map that preserves the distance between points) if `α` is a subsingleton. A subsingleton is a type that has at most one element. This theorem implies that in a subsingleton, where all elements are indistinguishable, all functions preserve the distance, since there's essentially only one point to map.
More concisely: If `α` and `β` are PseudoEMetricSpaces and `α` is a subsingleton, then any function from `α` to `β` is an isometry.
|
IsometryEquiv.surjective
theorem IsometryEquiv.surjective :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β),
Function.Surjective ⇑h
The theorem `IsometryEquiv.surjective` states that for any two types `α` and `β`, which are provided with pseudo-emetric space structures, if there exists an isometry equivalence `h` from `α` to `β`, then the function corresponding to this isometry equivalence (`h`) is surjective. In other words, for every element in `β`, there is an element in `α` such that when the isometry equivalence `h` is applied to the element from `α`, it equals the given element in `β`.
More concisely: Given isometry equivalences between pseudo-metric spaces `α` and `β`, if the equivalence is surjective, then every element in `β` has an equivalent element in `α`.
|
IsometryEquiv.preimage_symm
theorem IsometryEquiv.preimage_symm :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β),
Set.preimage ⇑h.symm = Set.image ⇑h
This theorem states that for any two types `α` and `β`, both equipped with a pseudo emetric space structure, given an isometric isomorphism `h` from `α` to `β`, the preimage under the inverse isomorphism is equal to the image under the original isomorphism.
In the context of mathematics, this theorem can be interpreted as follows: if you take a set in `β`, apply the inverse isometric isomorphism and find the corresponding set in `α`, it would be the same as if you started with the corresponding set in `α` and applied the original isometric isomorphism to find the set in `β`. This emphasizes the bijective nature of the isometric isomorphism.
More concisely: For any isometric isomorphisms between pseudo metric spaces `h: α → β` and `g: β → α`, we have `g⁻¹(h(A)) = A` for any set `A` in `α`.
|
Isometry.comp
theorem Isometry.comp :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
[inst_2 : PseudoEMetricSpace γ] {g : β → γ} {f : α → β}, Isometry g → Isometry f → Isometry (g ∘ f)
This theorem states that the composition of two isometries is also an isometry. In a more detailed explanation, given two pseudoemetric spaces (which are types `α`, `β`, and `γ`), and two functions `f : α → β` and `g : β → γ` that are isometries (i.e., they preserve the edistance between points in their respective spaces), then their composition `g ∘ f : α → γ` is also an isometry. This means that for any two points `x1` and `x2` in space `α`, the edistance between the images of these two points under the composed map `g ∘ f` is equal to the edistance between `x1` and `x2`.
More concisely: The composition of two isometries is an isometry.
|
Mathlib.Topology.MetricSpace.Isometry._auxLemma.4
theorem Mathlib.Topology.MetricSpace.Isometry._auxLemma.4 : ∀ {r₁ r₂ : NNReal}, (↑r₁ = ↑r₂) = (r₁ = r₂)
This theorem, referred to as `Mathlib.Topology.MetricSpace.Isometry._auxLemma.4`, states that for any two nonnegative real numbers `r₁` and `r₂` (denoted in Lean 4 as `{r₁ r₂ : NNReal}`), the equality of these two numbers in their lifted form (represented as `↑r₁ = ↑r₂`) is equivalent to the equality of these two numbers in their original form (represented as `r₁ = r₂`). The lifted form refers to the representation of these numbers in a different type or space.
More concisely: The theorem `Mathlib.Topology.MetricSpace.Isometry._auxLemma.4` in Lean 4 states that for any nonnegative real numbers `r₁` and `r₂`, `↑r₁ = ↑r₂` if and only if `r₁ = r₂`.
|
Isometry.diam_image
theorem Isometry.diam_image :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
Isometry f → ∀ (s : Set α), Metric.diam (f '' s) = Metric.diam s
This theorem states that an isometry preserves the diameter in pseudometric spaces. More precisely, for any two types `α` and `β` that are pseudometric spaces, for any function `f` from `α` to `β` that is an isometry, and for any set `s` of type `α`, the diameter of the image set under the function `f` is equal to the diameter of the original set `s`. In mathematical terms, if `diam` denotes the diameter of a set in a pseudometric space, `f` is an isometry, and `s` is a set in the space, then `diam(f(s)) = diam(s)`.
More concisely: In pseudometric spaces, an isometry preserves the diameter of sets, i.e., the diameter of the image of a set under an isometry equals the diameter of the original set.
|
Isometry.uniformEmbedding
theorem Isometry.uniformEmbedding :
∀ {α : Type u} {β : Type v} [inst : EMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
Isometry f → UniformEmbedding f
The theorem `Isometry.uniformEmbedding` states that for any function `f` from a type `α` to a type `β`, where `α` is an extended metric space (`EMetricSpace`) and `β` is a pseudo extended metric space (`PseudoEMetricSpace`), if `f` preserves the extended distance (`edist`) between any two points in `α` (i.e., `f` is an isometry), then `f` is a uniform embedding. A uniform embedding is a function that preserves the uniform structure of the space. In other words, isometries from extended metric spaces to pseudo extended metric spaces are always uniform embeddings.
More concisely: If `f: α → β` is an isometry between extended metric spaces `α` and pseudo extended metric spaces `β`, then `f` is a uniform embedding.
|