LipschitzWith.properSpace
theorem LipschitzWith.properSpace :
∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : MetricSpace β] [inst_2 : ProperSpace β]
{K : NNReal} {f : α ≃ₜ β}, LipschitzWith K ⇑f → ProperSpace α
The theorem `LipschitzWith.properSpace` states that given two types `α` and `β` (representing mathematical spaces), where `α` is a PseudoMetricSpace and `β` is both a MetricSpace and a ProperSpace, along with a non-negative real number `K` and a bijective function `f` (which is a homeomorphism) from `α` to `β`, if function `f` is Lipschitz continuous with constant `K`, then `α` is a ProperSpace. In other words, if we have a Lipschitz continuous homeomorphism from a space to a ProperSpace, then the original space is also a ProperSpace. In the context of metric spaces, a ProperSpace is a space where every closed ball is compact.
More concisely: If `α` is a PseudoMetricSpace, `β` is a MetricSpace and ProperSpace, `f: α → β` is a bijective Lipschitz homeomorphism with constant `K`, then `α` is a ProperSpace.
|
AntilipschitzWith.tendsto_cobounded
theorem AntilipschitzWith.tendsto_cobounded :
∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal}
{f : α → β}, AntilipschitzWith K f → Filter.Tendsto f (Bornology.cobounded α) (Bornology.cobounded β)
The theorem `AntilipschitzWith.tendsto_cobounded` states that for all types `α` and `β` which have a pseudo metric space structure, for a given nonnegative real number `K` and a function `f` mapping `α` to `β`, if `f` is `AntilipschitzWith K`, then `f` tends to the filter of cobounded sets in the bornology of `β` when the filter of cobounded sets in the bornology of `α` is considered. In other words, for any neighborhood of cobounded sets in `β`, the preimage of this neighborhood under `f` is a neighborhood of cobounded sets in `α`. This implies that the function `f` controls how points in `α` are spread out in `β` when considering cobounded sets.
More concisely: If `f` is an `AntilipschitzWith` function from a pseudo metric space `(α, dα)` to another pseudo metric space `(β, dβ)` with constant `K`, then the preimages of neighborhoods of cobounded sets in `β` under `f` are neighborhoods of cobounded sets in `α`.
|
AntilipschitzWith.of_le_mul_dist
theorem AntilipschitzWith.of_le_mul_dist :
∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal}
{f : α → β}, (∀ (x y : α), dist x y ≤ ↑K * dist (f x) (f y)) → AntilipschitzWith K f
This theorem states that for any two types `α` and `β` equipped with a pseudo metric space structure, and for any nonnegative real number `K` and function `f` from `α` to `β`, if for every pair of elements `x` and `y` of `α`, the distance between `x` and `y` is less than or equal to `K` times the distance between `f(x)` and `f(y)`, then `f` is `AntilipschitzWith` `K`. The `AntilipschitzWith` condition means that the function `f` doesn't increase distances between points more than a certain factor `K`.
More concisely: If `α` and `β` are type spaces equipped with pseudo metrics, and for all `x, y ∈ α`, the distance `d(x, y)` is less than or equal to non-negative real number `K` times the distance `d(f(x), f(y))`, then `f : α → β` is an antip daschsitz function with constant `K`.
|
AntilipschitzWith.properSpace
theorem AntilipschitzWith.properSpace :
∀ {β : Type u_2} [inst : PseudoMetricSpace β] {α : Type u_4} [inst_1 : MetricSpace α] {K : NNReal} {f : α → β}
[inst_2 : ProperSpace α], AntilipschitzWith K f → Continuous f → Function.Surjective f → ProperSpace β
The theorem "AntilipschitzWith.properSpace" states that for any nonnegative real number `K`, and any function `f` from a type `α` to another type `β`, if `α` is a proper metric space, `f` is an Antilipschitz function with constant `K`, `f` is continuous, and `f` is surjective (i.e., every element of `β` is an image of some element in `α` under `f`), then `β` is also a proper metric space.
In mathematical terms, a proper space is a metric space in which every closed ball is compact. Antilipschitz functions, in this context, are mappings where the distance between two points in the domain is not more than `K` times the distance between their images in the codomain. Hence, the theorem essentially states that an expanding onto map (an Antilipschitz, surjective function) from a proper space results in a proper space.
More concisely: If `α` is a proper metric space, `f: α → β` is a continuous, surjective Antilipschitz function with constant `K`, then `β` is a proper metric space.
|
AntilipschitzWith.uniformInducing
theorem AntilipschitzWith.uniformInducing :
∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal}
{f : α → β}, AntilipschitzWith K f → UniformContinuous f → UniformInducing f
The theorem `AntilipschitzWith.uniformInducing` states that for any two types `α` and `β` equipped with the pseudo-emetric space structure, a non-negative real number `K`, and a function `f` from `α` to `β`, if `f` is `AntilipschitzWith` `K` and `f` is also uniformly continuous, then `f` is uniform inducing.
In more natural language, this theorem says that if a function `f` from one metric space to another is Antilipschitz (meaning that the distance between any two points in the input space is at most `K` times the distance between their images in the output space) and uniformly continuous (meaning that if two points in the input space are sufficiently close to each other, their images under `f` will also be close to each other), then `f` is uniform inducing, which implies that the uniformity (topological structure that allows us to speak about "closeness" of points) on the input space can be recovered from the uniformity on the output space via `f`.
More concisely: If a function between two pseudo-metric spaces is Antilipschitz with a constant K and uniformly continuous, then it is uniformly inducing.
|
AntilipschitzWith.subsingleton
theorem AntilipschitzWith.subsingleton :
∀ {α : Type u_4} {β : Type u_5} [inst : EMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
AntilipschitzWith 0 f → Subsingleton α
The theorem states that if `f`, a function mapping from type `α` to type `β`, is `0`-antilipschitz, then `α` is a subsingleton. Here, `f` being `0`-antilipschitz means that for any two points `x` and `y` in `α`, the extended (possibly infinite) distance between `x` and `y` is less than or equal to `0` times the extended distance between `f(x)` and `f(y)` in `β`. A type `α` being a subsingleton means that there is at most one element in `α`. So, essentially, the theorem establishes that a `0`-antilipschitz function `f` collapses its domain `α` to at most one point, making `α` a subsingleton.
More concisely: If `f` is a `0`-antilipschitz function from a type `α`, then `α` is a subsingleton.
|
AntilipschitzWith.uniformEmbedding
theorem AntilipschitzWith.uniformEmbedding :
∀ {α : Type u_4} {β : Type u_5} [inst : EMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
AntilipschitzWith K f → UniformContinuous f → UniformEmbedding f
This theorem states that for any two types `α` and `β`, where `α` is an extended metric space and `β` is a pseudo-extended metric space, if a function `f` from `α` to `β` is Antilipschitz with a nonnegative real number `K` and is uniformly continuous, then `f` is a uniform embedding. In other words, if for any two points `x` and `y` in `α`, the extended distance between `x` and `y` is less than or equal to `K` times the extended distance between `f(x)` and `f(y)`, and if `f` is such that for any arbitrarily close points `x` and `y` in `α`, their images `f(x)` and `f(y)` are also arbitrarily close in `β`, then `f` also preserves the uniform structure, i.e., the relationships between all points and their neighborhoods, when mapping from `α` to `β`.
More concisely: If `f` is a uniformly continuous, Antilipschitz function from an extended metric space `α` to a pseudo-extended metric space `β` with constant `K`, then `f` is a uniform embedding.
|
AntilipschitzWith.of_le_mul_nndist
theorem AntilipschitzWith.of_le_mul_nndist :
∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal}
{f : α → β}, (∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)) → AntilipschitzWith K f
This theorem, named `AntilipschitzWith.of_le_mul_nndist`, states that for any two types `α` and `β` that are pseudometric spaces and a nonnegative real number `K`, if a function `f` from `α` to `β` satisfies the property that for any two points `x` and `y` in `α` the nonnegative distance (`nndist`) between `x` and `y` is less than or equal to `K` times the nonnegative distance between `f(x)` and `f(y)`, then the function `f` is Antilipschitz with constant `K`. An Antilipschitz function is one where the distance between any two points in the output space is not expanded by more than a certain factor compared to their distance in the input space.
More concisely: If a function between two pseudometric spaces satisfies the property that the distance between any two points in the input space is less than or equal to a constant times the distance between their images, then the function is Antilipschitz with that constant.
|
AntilipschitzWith.le_mul_nndist
theorem AntilipschitzWith.le_mul_nndist :
∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal}
{f : α → β}, AntilipschitzWith K f → ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)
The theorem `AntilipschitzWith.le_mul_nndist` states that for any two points `x` and `y` in a pseudometric space `α`, and a function `f` from `α` to another pseudometric space `β`, if `f` is Antilipschitz with a non-negative real number `K` (i.e., the extended distance between `x` and `y` is less than or equal to `K` times the extended distance between `f(x)` and `f(y)`), then the non-negative distance between `x` and `y` is also less than or equal to `K` times the non-negative distance between `f(x)` and `f(y)`. In mathematical terms, given $x, y \in α$, if $f : α \to β$ is Antilipschitz with a constant $K$, then $d(x, y) \leq K * d(f(x), f(y))$, where $d(., .)$ is the non-negative distance.
More concisely: Given a pseudometric space `α`, a function `f : α → β` that is Antilipschitz with constant `K`, and any `x, y ∈ α`, the non-negative distance `d(x, y)` is less than or equal to `K` times the non-negative distance `d(f(x), f(y))`.
|
AntilipschitzWith.isBounded_preimage
theorem AntilipschitzWith.isBounded_preimage :
∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal}
{f : α → β}, AntilipschitzWith K f → ∀ {s : Set β}, Bornology.IsBounded s → Bornology.IsBounded (f ⁻¹' s)
The theorem `AntilipschitzWith.isBounded_preimage` states that for any two types `α` and `β` equipped with pseudo metric spaces, a nonnegative real number `K`, and a function `f` from `α` to `β` that is Anti-lipschitz with `K`, if a set `s` of type `β` is bounded relative to the ambient bornology on `β`, then the preimage of `s` under the function `f` is also bounded relative to the ambient bornology on `α`.
In simpler terms, this theorem asserts that if a function doesn't stretch distances by more than a factor of `K` (it's Anti-lipschitz), and if a set in the target space is bounded, then the set of points in the source space that map into this bounded set is also bounded.
More concisely: If `f` is an Anti-lipschitz function from a pseudo metric space `(α, d₁)` to another pseudo metric space `(β, d₂)` with constant `K`, and `s ⊆ β` is a bounded set, then the preimage `f⁻¹(s) ⊆ α` is also a bounded set.
|
AntilipschitzWith.injective
theorem AntilipschitzWith.injective :
∀ {α : Type u_4} {β : Type u_5} [inst : EMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
AntilipschitzWith K f → Function.Injective f
The theorem `AntilipschitzWith.injective` states that, for any two types `α` and `β` where `α` is an extended metric space and `β` is a pseudo extended metric space, and given a nonnegative real number `K` and a function `f` from `α` to `β`, if the function `f` has the property `AntilipschitzWith K`, meaning that the extended distance between any two points in `α` is less than or equal to `K` times the extended distance between their images under `f` in `β`, then the function `f` is injective, that is, equal images under `f` have equal preimages. In other words, if a function distorts distances by a bounded factor, then it does not map distinct points to the same point.
More concisely: If a function between extended metric spaces with the Antilipschitz property with constant K is non-expanding, then it is injective.
|
AntilipschitzWith.isBounded_of_image2_left
theorem AntilipschitzWith.isBounded_of_image2_left :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
[inst_2 : PseudoMetricSpace γ] (f : α → β → γ) {K₁ : NNReal},
(∀ (b : β), AntilipschitzWith K₁ fun a => f a b) →
∀ {s : Set α} {t : Set β},
Bornology.IsBounded (Set.image2 f s t) → Bornology.IsBounded s ∨ Bornology.IsBounded t
This theorem states that for any types `α`, `β`, and `γ` with pseudometric space structures, given a binary function `f : α → β → γ` and a nonnegative real number `K₁`, if for all `b` in `β`, the function `a => f a b` is `K₁`-Antilipschitz, then for any sets `s` of `α` and `t` of `β`, if the image of the sets `s` and `t` under the function `f` is bounded (in the sense of bornology), then either the set `s` is bounded or the set `t` is bounded. Here, a function is `K₁`-Antilipschitz if the extended distance between any two points `x` and `y` is less than or equal to `K₁` times the extended distance between `f(x)` and `f(y)`. Boundedness of a set is defined relative to the ambient bornology.
More concisely: Given types `α`, `β`, and `γ` with pseudometric spaces, a `K₁`-Antilipschitz function `f : α → β → γ`, and sets `s ⊆ α` and `t ⊆ β` with bounded images under `f`, either `s` or `t` is bounded.
|
Mathlib.Topology.MetricSpace.Antilipschitz._auxLemma.1
theorem Mathlib.Topology.MetricSpace.Antilipschitz._auxLemma.1 :
∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal}
{f : α → β}, AntilipschitzWith K f = ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)
The theorem `Mathlib.Topology.MetricSpace.Antilipschitz._auxLemma.1` states that for all types `α` and `β` that are pseudo metric spaces, for a nonnegative real number `K` and a function `f` from `α` to `β`, `f` is `AntilipschitzWith` `K` if and only if the distance from `x` to `y` in the space `α` is less than or equal to `K` times the distance from `f(x)` to `f(y)` in the space `β`. This theorem explicitly describes the property of a function being Antilipschitz with respect to a certain constant, which is related to the function not expanding distances between any two points.
More concisely: A function between two pseudo metric spaces is Antilipschitz with constant K if and only if the distance between any two points in the first space is less than or equal to K times the distance between their images in the second space.
|
AntilipschitzWith.le_mul_dist
theorem AntilipschitzWith.le_mul_dist :
∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal}
{f : α → β}, AntilipschitzWith K f → ∀ (x y : α), dist x y ≤ ↑K * dist (f x) (f y)
The theorem `AntilipschitzWith.le_mul_dist` states that if a function `f` from a pseudo-metric space `α` to a pseudo-metric space `β` is `AntilipschitzWith` a nonnegative real number `K`, then for any two points `x` and `y` in `α`, the distance between `x` and `y` is less than or equal to `K` times the distance between `f(x)` and `f(y)`. This is essentially saying that the function does not increase distances by more than a factor of `K`.
More concisely: For any AntilipschitzWith (K > 0) function f from a pseudo-metric space (α, dα) to another pseudo-metric space (β, dβ), it holds that dα(x, y) ≤ K × dβ(f(x), f(y)) for all x, y in α.
|