Dilation.injective
theorem Dilation.injective :
∀ {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace β] {α : Type u_6} [inst_1 : EMetricSpace α]
[inst_2 : FunLike F α β] [inst : DilationClass F α β] (f : F), Function.Injective ⇑f
The theorem `Dilation.injective` states that for any types `β`, `F`, and `α`, where `β` is a pseudo-emetric space and `α` is an emetric space, if `F` has a function-like structure from `α` to `β` and also has a dilation structure, then any function `f` of type `F` is injective. In other words, if `f(x) = f(y)`, then it must be the case that `x = y`. This is a property of dilations in emetric spaces.
More concisely: If `F` is a function-like type from an emetric space `α` to a pseudo-metric space `β` with a dilation structure, then `F` is injective.
|
Dilation.mapsTo_closedBall
theorem Dilation.mapsTo_closedBall :
∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
[inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F) (x : α) (r' : ℝ),
Set.MapsTo (⇑f) (Metric.closedBall x r') (Metric.closedBall (f x) (↑(Dilation.ratio f) * r'))
This theorem states that for any dilation function `f`, in any pseudometric spaces `α` and `β`, and for any element `x` in `α` and real number `r'`, the function `f` maps the closed ball around `x` with radius `r'` in `α` to the closed ball around `f(x)` with radius equal to `r'` scaled by the ratio of the dilation function `f` in `β`. Here, a closed ball around a point is the set of all points whose distance from the center is less than or equal to the radius, and the dilation function is a function that scales distances between points.
More concisely: For any dilation function `f` and real number `r`, the closed ball around `x` with radius `r` in metric space `α` is mapped to the closed ball around `f(x)` with radius `r / |f|` in metric space `β`, where `|f|` denotes the ratio of the dilation function `f` in `β`.
|
Dilation.ext
theorem Dilation.ext :
∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f g : α →ᵈ β},
(∀ (x : α), f x = g x) → f = g
This theorem, `Dilation.ext`, states that for any two dilation functions `f` and `g` within a pseudo emetric space, if for all `x` in domain type `α`, `f(x)` equals `g(x)`, then `f` equals `g`. In other words, if two dilation functions produce the same output for every input in the domain, they are the same function. The pseudo emetric space ensures that the distances between points in the space adhere to certain conditions, like symmetry and triangle inequality.
More concisely: In a pseudo-metric space, if two dilation functions are equal on all points in their domain, then they are identical functions.
|
Dilation.mapsTo_emetric_closedBall
theorem Dilation.mapsTo_emetric_closedBall :
∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
[inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F) (x : α) (r' : ENNReal),
Set.MapsTo (⇑f) (EMetric.closedBall x r') (EMetric.closedBall (f x) (↑(Dilation.ratio f) * r'))
The theorem `Dilation.mapsTo_emetric_closedBall` states that for any types `α`, `β`, and `F`, where `α` and `β` are pseudo emetric spaces, `F` is a function from `α` to `β`, and `F` is a dilation function, a dilation `f` maps the closed ball in `α` centered at `x` with radius `r'` to the closed ball in `β` centered at `f(x)` with radius equal to the dilation ratio of `f` times `r'`. In other words, a dilation function not only maps the points inside a closed ball to another closed ball but also scales the radius of the ball by its dilation ratio.
More concisely: For any pseudo metric spaces α and β, a dilation function F : α → β from a metric space (α, dα) to (β, dβ) with dilation ratio λ, maps the closed ball B(x, r) in (α, dα) to the closed ball B(F(x), λ \* r) in (β, dβ).
|
Dilation.ratio_comp'
theorem Dilation.ratio_comp' :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
[inst_2 : PseudoEMetricSpace γ] {g : β →ᵈ γ} {f : α →ᵈ β},
(∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ⊤) → Dilation.ratio (g.comp f) = Dilation.ratio g * Dilation.ratio f
The theorem `Dilation.ratio_comp'` states that, for two dilation functions `f` and `g` acting on pseudo-emetric spaces `α`, `β`, and `γ`, the ratio of the composition `g.comp f` is the product of the individual ratios of `g` and `f`. This assumes that there exist two points in `α` with an extended distance that is neither `0` nor infinity. If this were not the case, both the composition's ratio and `f`'s ratio would be `1`, while `g`'s ratio could be any number. This theorem is applicable to general metric spaces, but there is also a version `Dilation.ratio_comp` for only nontrivial metric spaces.
More concisely: Given dilation functions `f` and `g` on pseudo-metric spaces `α`, `β`, and `γ` with points having a finite extended distance, the ratio of their composition `g.comp f` equals the product of the ratios of `g` and `f`.
|
Dilation.ratio_unique_of_dist_ne_zero
theorem Dilation.ratio_unique_of_dist_ne_zero :
∀ {α : Type u_7} {β : Type u_8} {F : Type u_6} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
[inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] {f : F} {x y : α} {r : NNReal},
dist x y ≠ 0 → dist (f x) (f y) = ↑r * dist x y → r = Dilation.ratio f
This theorem, named `Dilation.ratio_unique_of_dist_ne_zero`, states that for any two points with nonzero finite distance in a pseudometric spaces `α` and `β`, the ratio of a dilation `f` is equal to the distance ratio of these two points. Here, the dilation `f` is a function-like structure `F` that maps `α` to `β`. This is achieved under the conditions that `α` and `β` are pseudometric spaces, `F` is a function-like structure from `α` to `β`, and `f` is a dilation from `α` to `β`. In other words, if the distance between `x` and `y` is not zero and the distance between `f(x)` and `f(y)` is equal to the nonnegative real number `r` multiplied by the distance between `x` and `y`, then `r` is equal to the dilation ratio of `f`.
More concisely: Given two points in pseudometric spaces with nonzero finite distance, the dilation ratio of a dilation function between the spaces is equal to the distance ratio of the points if and only if the distances are proportional.
|
Dilation.uniformEmbedding
theorem Dilation.uniformEmbedding :
∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : EMetricSpace α] [inst_1 : FunLike F α β]
[inst_2 : PseudoEMetricSpace β] [inst_3 : DilationClass F α β] (f : F), UniformEmbedding ⇑f
This theorem states that for any types `α`, `β`, and `F`, if `α` is an extended metric space, `F` is a function-like structure from `α` to `β`, `β` is a pseudo extended metric space, and `F` satisfies the dilation property, then any term `f` of type `F` is a uniform embedding. In other words, the function `f` preserves the distances between the points in `α` when it maps them to `β`, and also provides a one-to-one correspondence between `α` and its image in `β`. This is a key property in the theory of metric spaces and their embeddings.
More concisely: If `α` is an extended metric space, `F` is a function-like structure from `α` to a pseudo extended metric space `β` satisfying the dilation property, then `F` is a uniform embedding, i.e., it preserves distances and establishes a bijective mapping between `α` and its image in `β`.
|
Dilation.diam_image
theorem Dilation.diam_image :
∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
[inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F) (s : Set α),
Metric.diam (⇑f '' s) = ↑(Dilation.ratio f) * Metric.diam s
This theorem, named `Dilation.diam_image`, states that in pseudometric spaces, a dilation operation scales the diameter of a set by the ratio of the dilation. Specifically, for any pseudometric spaces `α` and `β`, any function `f` of type `F` that behaves like a function from `α` to `β` and satisfies the properties of a dilation, and any set `s` of elements of type `α`, the diameter of the image of the set `s` under the function `f` is equal to the ratio of the dilation `f` times the diameter of the set `s`.
More concisely: Given a pseudometric space `α`, a dilation function `f` from `α` to itself with ratio `r`, and a set `s` in `α`, the diameter of `f`'s image of `s` is equal to `r` times the diameter of `s`.
|
Dilation.comap_cobounded
theorem Dilation.comap_cobounded :
∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
[inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F),
Filter.comap (⇑f) (Bornology.cobounded β) = Bornology.cobounded α
The theorem `Dilation.comap_cobounded` states that for any types `α`, `β`, and `F`, given that `α` and `β` are both pseudo metric spaces, `F` is a function-like from `α` to `β`, and `F` is a dilation class from `α` to `β`, then for any function `f` of type `F`, the comap (preimage) of the filter of cobounded sets of `β` under `f` is equal to the filter of cobounded sets of `α`. In other words, pulling back the set of cobounded subsets of `β` via the function `f` gives us the set of cobounded subsets of `α`. This theorem provides a connection between the bornologies (a structure defining "bounded" subsets) of two pseudo metric spaces through a function that satisfies certain properties.
More concisely: Given functions between pseudo metric spaces that preserve cobounded sets and are dilations, the preimages of cobounded sets under these functions form the same filter as the cobounded sets in the domain.
|
Dilation.ratio_comp
theorem Dilation.ratio_comp :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MetricSpace α] [inst_1 : Nontrivial α]
[inst_2 : PseudoEMetricSpace β] [inst_3 : PseudoEMetricSpace γ] {g : β →ᵈ γ} {f : α →ᵈ β},
Dilation.ratio (g.comp f) = Dilation.ratio g * Dilation.ratio f
The theorem `Dilation.ratio_comp` states that for any two dilations `f` and `g`, where `f` is a dilation from a nontrivial metric space `α` to a pseudoemetric space `β`, and `g` is a dilation from `β` to another pseudoemetric space `γ`, the ratio of the composite function `g.comp f` (i.e., the dilation obtained by first applying `f` then `g`) is equal to the product of the ratios of `g` and `f`. The theorem is only valid when `α` is a nontrivial metric space; otherwise, the ratios of `f` and `g.comp f` would both be equal to 1 but the ratio of `g` could take any value. For more general spaces, see the theorem `Dilation.ratio_comp'`.
More concisely: For any dilations \(f:\alpha \to \beta\) from a nontrivial metric space \(\alpha\) to a pseudometric space \(\beta\), and \(g:\beta \to \gamma\) from \(\beta\) to another pseudometric space \(\gamma\), the ratio of the composite dilation \(g \circ f\) equals the product of the ratios of \(g\) and \(f\).
|
Dilation.mapsTo_ball
theorem Dilation.mapsTo_ball :
∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
[inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F) (x : α) (r' : ℝ),
Set.MapsTo (⇑f) (Metric.ball x r') (Metric.ball (f x) (↑(Dilation.ratio f) * r'))
This theorem, `Dilation.mapsTo_ball`, states that for any pseudo metric spaces `α` and `β`, and for any function `f` that is a dilation (i.e., a function that scales distances), the application of `f` maps a ball in `α` centered at `x` with radius `r'` to a ball in `β` centered at `f(x)` with radius scaled by the dilation ratio of `f`. In other words, a dilation transforms balls into balls while scaling their radii by the dilation ratio.
More concisely: For any pseudo metric spaces α and β, and any dilation function f: α → β, the image of a ball in α centered at x with radius r under f is a ball in β centered at f(x) with radius scaled by the dilation ratio of f.
|
Dilation.uniformInducing
theorem Dilation.uniformInducing :
∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
[inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F), UniformInducing ⇑f
The theorem `Dilation.uniformInducing` states that for any types `α`, `β`, and `F`, if `α` and `β` are pseudo emetric spaces (generalization of the concept of a metric space where distances can be infinite), `F` is a function-like from `α` to `β`, and `F` satisfies the conditions of the `DilationClass`, then for any function `f` of type `F`, the function `f` induces a uniform structure on `α`. In simpler words, the application of the function `f` results in uniformly distributed points in `α`.
More concisely: Given types `α`, `β`, and a function-like `F` from `α` to `β` between pseudo-metric spaces `α` and `β`, if `F` satisfies the conditions of `DilationClass`, then `F` induces a uniform structure on `α`.
|
Dilation.ratio_unique_of_nndist_ne_zero
theorem Dilation.ratio_unique_of_nndist_ne_zero :
∀ {α : Type u_6} {β : Type u_7} {F : Type u_8} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
[inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] {f : F} {x y : α} {r : NNReal},
nndist x y ≠ 0 → nndist (f x) (f y) = r * nndist x y → r = Dilation.ratio f
The theorem `Dilation.ratio_unique_of_nndist_ne_zero` states that for any two points `x` and `y` in a PseudoMetricSpace `α` (where the distances between points are non-negative real numbers), under a function `f` of type `F` that behaves like a dilation (i.e., it scales distances), if the non-negative distance `nndist` between `x` and `y` is not zero, then the non-negative distance between the images of these points under `f` is equal to some real number `r` times the original distance. In this case, `r` is equal to the `ratio` of the dilation `f`. In other words, this theorem asserts the uniqueness of the ratio of a dilation in terms of how it scales distances between points.
More concisely: Given a PseudoMetricSpace α and a dilation function f : α → α with non-zero distance nndist(x, y) between points x and y, the ratio of the distances d(fx, fy) and nndist(x, y) is unique and equal to the dilation ratio of f.
|
Dilation.ediam_range
theorem Dilation.ediam_range :
∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
[inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F),
EMetric.diam (Set.range ⇑f) = ↑(Dilation.ratio f) * EMetric.diam Set.univ
This theorem states that for any dilation `f` in a pseudoemetric space, the diameter of the range of `f` is equal to the ratio of the dilation `f` times the diameter of the universal set. In simpler terms, a dilation operation scales the diameter of the set of all outputs of the function (which the dilation is performed on) by the ratio associated with the dilation. This applies in pseudoemetric spaces, which are mathematical structures that generalize the notion of a metric space, allowing for some distances to be infinite.
More concisely: In a pseudometric space, the diameter of the image of a dilation function is equal to the dilation factor times the diameter of the underlying set.
|
Dilation.edist_eq
theorem Dilation.edist_eq :
∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
[inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F) (x y : α),
edist (f x) (f y) = ↑(Dilation.ratio f) * edist x y
This theorem, named `Dilation.edist_eq`, states that for any types `α`, `β`, and `F` where `α` and `β` are pseudo-emetric spaces and `F` is a function-like structure that maps `α` to `β` and is also a dilation, any function `f` of type `F`, and any elements `x` and `y` of type `α`, the extended distance between `f(x)` and `f(y)` in the pseudo-emetric space `β` is equal to the dilation ratio of `f` times the extended distance between `x` and `y` in the pseudo-emetric space `α`. In mathematical terms, `edist (f x) (f y) = ↑(Dilation.ratio f) * edist x y`. This theorem essentially describes how a dilation function impacts the distances in a pseudo-emetric space.
More concisely: The extended distance between the images of two points under a dilation function is equal to the dilation ratio times the extended distance between the original points in a pseudo-metric space.
|
Dilation.toContinuous
theorem Dilation.toContinuous :
∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
[inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F), Continuous ⇑f
The theorem `Dilation.toContinuous` states that for any types `α`, `β`, and `F`, if `α` and `β` are pseudo emetric spaces, `F` is a function-like structure from `α` to `β`, and `F` satisfies the properties of a dilation class, then any instance `f` of type `F` is a continuous function. In other words, a dilation (a transformation that alters the size of an object without changing its shape or orientation) is always a continuous operation with respect to the pseudo emetric space structure.
More concisely: If `F` is a function-like structure from a pseudo metric space `α` to a pseudo metric space `β`, and `F` satisfies the properties of a dilation class, then every instance `f` of `F` is a continuous function.
|
Dilation.mapsTo_sphere
theorem Dilation.mapsTo_sphere :
∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
[inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F) (x : α) (r' : ℝ),
Set.MapsTo (⇑f) (Metric.sphere x r') (Metric.sphere (f x) (↑(Dilation.ratio f) * r'))
The theorem `Dilation.mapsTo_sphere` states that for any dilation `f` in a pseudo metric space, it transforms spheres to spheres while scaling the radius by the dilation ratio of `f`. More specifically, given a point `x` and a real number `r'`, the image under `f` of the sphere centered at `x` with radius `r'` is the sphere centered at `f(x)` with radius scaled by the ratio of `f` times `r'`.
More concisely: For any dilation function f in a pseudo-metric space and point x with real radius r', the image of the sphere centered at x with radius r' under f is a sphere centered at f(x) with scaled radius r' multiplied by the dilation ratio of f.
|
Dilation.ratio_unique
theorem Dilation.ratio_unique :
∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
[inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] {f : F} {x y : α} {r : NNReal},
edist x y ≠ 0 → edist x y ≠ ⊤ → edist (f x) (f y) = ↑r * edist x y → r = Dilation.ratio f
This theorem, `Dilation.ratio_unique`, states that for any two points with a nonzero and finite distance in a pseudo emetric space, the `ratio` of a dilation `f` is equal to the ratio of the distance between the images of the points under `f` and the original distance between the points. This applies for any function `f` that preserves distances (a dilation), as defined in the context of a `FunLike` function from the source to the target space, both of which are pseudo emetric spaces. The dilation's `ratio`, therefore, uniquely identifies the scaling of distances under the dilation.
More concisely: In a pseudo metric space, for any two points with nonzero and finite distance, the ratio of their distances under a dilation function (preserving distances) is equal to the dilation function's scaling factor.
|
Dilation.lipschitz
theorem Dilation.lipschitz :
∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
[inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F), LipschitzWith (Dilation.ratio f) ⇑f
This theorem states that for any types `α`, `β`, and `F`, where `α` and `β` are equipped with a pseudo-emetric space structure, and `F` is a function-like type from `α` to `β` that also has a dilation structure, any function `f` of type `F` is Lipschitz continuous with the dilation ratio of `f` as the Lipschitz constant. In other words, the extended distance between the images of any two points under `f` is less than or equal to the dilation ratio of `f` times the extended distance between the two points themselves.
More concisely: Given types `α` and `β` with pseudo-metric spaces structures, and a function-like type `F` from `α` to `β` with a dilation structure, any `F`-function `f` is Lipschitz continuous with Lipschitz constant equal to the dilation ratio of `f`.
|
Dilation.ratio_ne_zero
theorem Dilation.ratio_ne_zero :
∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
[inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F), Dilation.ratio f ≠ 0
The theorem `Dilation.ratio_ne_zero` states that for any types `α`, `β`, and `F`, in a context where `α` and `β` have a structure of pseudo e-metric spaces, `F` is a function-like object from `α` to `β`, and `F` satisfies the conditions to be a dilation class, the ratio of a dilation `f` of type `F` is never zero. In other words, in the given conditions, the ratio of dilation of any function is always a nonzero real number.
More concisely: In the context of pseudo metric spaces α, β, and a function-like object F from α to β that satisfies the conditions of a dilation class, the dilation ratio of any dilation f of type F is nonzero.
|
Dilation.mapsTo_emetric_ball
theorem Dilation.mapsTo_emetric_ball :
∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
[inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F) (x : α) (r : ENNReal),
Set.MapsTo (⇑f) (EMetric.ball x r) (EMetric.ball (f x) (↑(Dilation.ratio f) * r))
This theorem states that for any types `α`, `β`, and `F`, where `α` and `β` are pseudo e-metric spaces, `F` is a function-like object from `α` to `β`, and the dilation is defined for `F` in the context of `α` and `β`, a dilation function `f` maps balls in `α` to balls in `β` while scaling the radius by the `ratio f`. More specifically, for any ball centered at `x` with radius `r` in `α`, its image under `f` is a ball in `β` centered at `f(x)` with radius equal to `ratio f` times `r`.
More concisely: Given pseudo metric spaces `α` and `β`, a function-like object `F` from `α` to `β` with defined dilation, and a dilation function `f`, for any ball `B(x, r)` in `α`, `F(B(x, r)) = B(f(x), ratio f * r)` in `β`.
|
Dilation.closedEmbedding
theorem Dilation.closedEmbedding :
∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : EMetricSpace α] [inst_1 : FunLike F α β]
[inst_2 : CompleteSpace α] [inst_3 : EMetricSpace β] [inst_4 : DilationClass F α β] (f : F), ClosedEmbedding ⇑f
The theorem `Dilation.closedEmbedding` states that for all types `α`, `β`, and `F`, given `α` is a complete emetric space, `β` is an emetric space, terms of type `F` have an injective function-like coercion from `α` to `β`, and `F` dilates `α` to `β`, then any term `f` of type `F` is a closed embedding. In other words, if we have a dilation from a complete emetric space, it is guaranteed to be a closed embedding. A closed embedding is a function which not only injectively maps the spaces, but also the closure of any set under the function equals the closure of its image in the codomain.
More concisely: If `α` is a complete metric space, `β` is a metric space, `F` dilates `α` to `β` and maps `α` injectively into `β`, then every term of type `F` is a closed embedding from `α` to `β`.
|
Dilation.embedding
theorem Dilation.embedding :
∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : EMetricSpace α] [inst_1 : FunLike F α β]
[inst_2 : PseudoEMetricSpace β] [inst_3 : DilationClass F α β] (f : F), Embedding ⇑f
The theorem `Dilation.embedding` states that for any types `α`, `β`, and `F`, if `α` is an extended metric space, `F` is a function-like structure from `α` to `β`, `β` is a pseudo-extended metric space, and `F` is a dilation class from `α` to `β`, then any instance `f` of `F` is an embedding. In other words, a dilation from a metric space to a pseudo-extended metric space is always an embedding, where an embedding is a function that preserves the structure of the space. The function is injective and homeomorphic to its image, meaning that it maintains the properties of distance and continuity.
More concisely: Given types `α`, `β`, and `F`, if `α` is an extended metric space, `F` is a dilation class from `α` to the pseudo-extended metric space `β`, then any instance `f` of `F` is a metric space embedding.
|
Dilation.dist_eq
theorem Dilation.dist_eq :
∀ {α : Type u_6} {β : Type u_7} {F : Type u_8} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
[inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F) (x y : α),
dist (f x) (f y) = ↑(Dilation.ratio f) * dist x y
This theorem states that for any types `α`, `β`, and `F`, given that `α` and `β` are pseudometric spaces, `F` is a function-like from `α` to `β`, and `F` is a dilation class from `α` to `β`, for any function `f` of type `F` and any two points `x` and `y` in `α`, the distance between the images of `x` and `y` under `f` equals the dilation ratio of `f` times the distance between `x` and `y`. In other words, `f` scales the distances in `α` by its dilation ratio.
More concisely: Given functions `F` from type `α` to type `β` between pseudometric spaces `α` and `β`, if `F` is both a function-like and a dilation class, then for all `x` and `y` in `α`, `d(F(x) F(y)) = dilation_ratio(F) * d(x, y)`.
|
Dilation.antilipschitz
theorem Dilation.antilipschitz :
∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
[inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F), AntilipschitzWith (Dilation.ratio f)⁻¹ ⇑f
The theorem `Dilation.antilipschitz` states that for any types `α`, `β`, `F` and for any term `f` of type `F`, if `α` and `β` are pseudo emetric spaces, `F` is a function-like type from `α` to `β`, and `F` satisfies the dilation conditions, then the function `f` is antilipschitz with a constant equal to the inverse of the dilation ratio of `f`. In other words, the extended distance between any two points in the domain is bounded above by the inverse of the dilation ratio of `f` times the extended distance between the images of these two points under `f`.
More concisely: Given functions `f : α → β` between pseudo-metric spaces `(α, dα)` and `(β, dβ)`, if `f` is a dilation map with dilation ratio `r`, then `f` is an antilipschitz function with constant `1/r`.
|
Dilation.ediam_image
theorem Dilation.ediam_image :
∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
[inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F) (s : Set α),
EMetric.diam (⇑f '' s) = ↑(Dilation.ratio f) * EMetric.diam s
The theorem `Dilation.ediam_image` states that for any types `α` and `β`, and any type `F` which behaves functionally, all in a pseudometric space, given a dilation `f` from `α` to `β` and a set `s` of type `α`, the diameter of the image set after applying the dilation `f` is equal to the dilation ratio `f` times the diameter of the original set `s`. This implies that dilations scale the diameter of a set by the dilation's ratio in pseudoemetric spaces.
More concisely: Given a dilation function `f` between pseudometric spaces, the image of a set under `f` has diameter equal to the dilation ratio of `f` times the diameter of the original set.
|