UniformInducing.uniformContinuous
theorem UniformInducing.uniformContinuous :
∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
UniformInducing f → UniformContinuous f
The theorem `UniformInducing.uniformContinuous` states that for any two types `α` and `β`, each equipped with a uniform space structure (i.e., they both have a topology that allows the measurement of "closeness"), and given a function `f` from `α` to `β`, if `f` is uniform inducing (meaning it preserves the uniformity structure in the sense that the uniformity on `α` is the same as the preimage under `f` of the uniformity on `β`), then `f` is also uniformly continuous. In other words, if `f` is such that it preserves the "closeness" relationship from `α` to `β`, then for any two points in `α` that are sufficiently close, their images under `f` in `β` are also close, regardless of their actual location in `α`.
More concisely: If a function between two uniform spaces is uniformly inducing, then it is uniformly continuous.
|
uniformEmbedding_iff'
theorem uniformEmbedding_iff' :
∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
UniformEmbedding f ↔
Function.Injective f ∧ UniformContinuous f ∧ Filter.comap (Prod.map f f) (uniformity β) ≤ uniformity α
The theorem `uniformEmbedding_iff'` states that for any two types `α` and `β` having uniform space structures, and any function `f` from `α` to `β`, the function `f` is a uniform embedding if and only if it satisfies the following three conditions:
1) `f` is an injective function, meaning that `f x = f y` implies `x = y`.
2) `f` is uniformly continuous, which means that if `x` is sufficiently close to `y`, then `f x` is close to `f y` regardless of `x` and `y`'s location in `α`.
3) The filter obtained by applying the function `f` twice to the input (in other words, taking the product map of `f` and `f`) and then applying the preimage operation (comap) to the uniformity of `β` is less than or equal to the uniformity of `α`. In mathematical terms, `Filter.comap (Prod.map f f) (uniformity β) ≤ uniformity α`.
More concisely: A function between uniform spaces is a uniform embedding if and only if it is injective, uniformly continuous, and the image of their uniformities under the product map and preimage operation satisfies the inequality.
|
UniformInducing.isComplete_range
theorem UniformInducing.isComplete_range :
∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : CompleteSpace α]
{f : α → β}, UniformInducing f → IsComplete (Set.range f)
The theorem `UniformInducing.isComplete_range` states that for any two types `α` and `β`, which are equipped with uniform spaces, and given that `α` is a complete space, any function `f` from `α` to `β` which induces a uniform structure is a complete set. In other words, for a function `f: α → β`, if it is a uniform inducing function, the range (or the image) of the function `f`, denoted as `Set.range f`, forms a complete set. Here, a set is considered complete if any Cauchy filter on the set has a limit in the set itself.
More concisely: If `α` is a complete uniform space and `f: α → β` is a uniformly continuous function, then the range `Set.range f` of `f` is a complete set.
|
UniformEmbedding.inj
theorem UniformEmbedding.inj :
∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
UniformEmbedding f → Function.Injective f
The theorem states that for any two types `α` and `β`, if both types are equipped with a uniform space structure, then any function `f` from `α` to `β` that is a uniform embedding is also injective. In other words, if `f` is a uniform embedding (which preserves uniformity structure), then it has the property that whenever `f(x)` equals `f(y)`, it must be the case that `x` equals `y`. Hence, no two different points in `α` map to the same point in `β` under a uniform embedding.
More concisely: If `α` and `β` are uniform spaces and `f : α → β` is a uniform embedding, then `f` is injective.
|
IsComplete.completeSpace_coe
theorem IsComplete.completeSpace_coe :
∀ {α : Type u} [inst : UniformSpace α] {s : Set α}, IsComplete s → CompleteSpace ↑s
The theorem `IsComplete.completeSpace_coe` states that for any type `α` equipped with a uniform space structure and any set `s` of `α`, if `s` is complete (that is, every Cauchy filter `f` for which `s` belongs to `f` has a limit in `s`), then the type-cast of `s` to a uniform space is a complete space. In other words, if a set in a given uniform space is complete, then when viewed as its own uniform space, the set is a complete space.
More concisely: If a set in a uniform space is complete, then it is a complete uniform space.
|
completeSpace_coe_iff_isComplete
theorem completeSpace_coe_iff_isComplete :
∀ {α : Type u} [inst : UniformSpace α] {s : Set α}, CompleteSpace ↑s ↔ IsComplete s
This theorem states that for any type `α` equipped with a `UniformSpace` structure and for any set `s` of `α`, the set `s` is a complete space (i.e., every Cauchy filter on `s` has a limit in `s`) if and only if `s` is complete. In mathematical terms, a set `s` in a uniform space `α` is considered to be a complete space if every Cauchy filter of `s` converges to a limit within `s`, and this is equivalent to the condition that `s` itself is complete.
More concisely: A set `s` in a uniform space `α` is complete if and only if every Cauchy filter on `s` has a limit in `s`.
|
completeSpace_iff_isComplete_range
theorem completeSpace_iff_isComplete_range :
∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
UniformInducing f → (CompleteSpace α ↔ IsComplete (Set.range f))
This theorem establishes an equivalence for the completeness of a space in the context of uniform spaces and uniform inducing functions. Specifically, for any two types `α` and `β` that have uniform space structures, and a function `f` from `α` to `β` that induces a uniform space structure on `β`, the theorem states that `α` being a complete space is equivalent to the range of `f` being complete. In terms of mathematics, completeness here refers to the property that every Cauchy filter in the space has a limit within the space.
More concisely: For uniform spaces `α` and `β`, and a uniformly continuous function `f: α → β`, the space `α` is complete if and only if the range `f("α")` is complete.
|
uniformEmbedding_subtype_val
theorem uniformEmbedding_subtype_val :
∀ {α : Type u} [inst : UniformSpace α] {p : α → Prop}, UniformEmbedding Subtype.val
This theorem states that for any given type `α` equipped with a uniform space structure and a property `p` that `α` may satisfy, the function `Subtype.val` is a uniform embedding. `Subtype.val` is a function that takes a subtype (elements of type `α` satisfying property `p`) and returns the underlying element in `α`. In other words, this theorem asserts that the process of retrieving the underlying element from a subtype - under the conditions specified - preserves the uniformity structure.
More concisely: Given a uniform space `(α, d)` and a subtype `s : α set` defined by a property `p`, the function `Subtype.val` is a uniform embedding from `(s, d)|._` to `(α, d)`.
|
UniformInducing.inducing
theorem UniformInducing.inducing :
∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
UniformInducing f → Inducing f
This theorem states that for any two types `α` and `β` which have `UniformSpace` instances, any function `f` from `α` to `β` that induces a uniform structure is also inducing. In other words, if a function `f` is uniform inducing - meaning that the uniformity on `β` is the image under `f` of the uniformity on `α` - then it also preserves the topology, i.e., the preimage under `f` of an open set in `β` is open in `α`.
More concisely: If two types `α` and `β` have `UniformSpace` instances, and a function `f` from `α` to `β` induces a uniform structure and preserves the topology, then `f` is uniformly continuous. (In other words, a uniformly inducing function is also continuous.)
|
IsClosed.completeSpace_coe
theorem IsClosed.completeSpace_coe :
∀ {α : Type u} [inst : UniformSpace α] [inst_1 : CompleteSpace α] {s : Set α}, IsClosed s → CompleteSpace ↑s := by
sorry
This theorem asserts that for any type `α` equipped with a `UniformSpace` structure and a `CompleteSpace` structure, and for any set `s` of elements of type `α`, if `s` is a closed set, then the set `s` is also a complete space. In other words, if every Cauchy sequence of points in `s` has a limit that also lies in `s` (which is what it means for `s` to be closed), then every Cauchy sequence of points in `s` converges to some limit in `s` (which is what it means for `s` to be a complete space).
More concisely: If a closed subset of a complete and uniform space is equipped with the induced uniform structure, then it is a complete space.
|
UniformInducing.comap_uniformity
theorem UniformInducing.comap_uniformity :
∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
UniformInducing f → Filter.comap (fun x => (f x.1, f x.2)) (uniformity β) = uniformity α
This theorem states that, for a given function `f` from type `α` to `β` and given that both `α` and `β` are equipped with a uniform space structure, if `f` is a uniform inducing function, then the pullback of the uniformity filter on the codomain `β` under the map `(f x.1, f x.2)` is equal to the uniformity filter on the domain `α`. In simpler terms, it says that function `f` maps the uniformity of the domain into the uniformity of the codomain.
More concisely: If `f : α → β` is a uniformly continuous function between uniform spaces `(α, 𝄎α)` and `(β, 𝄎β)`, then `f⁁⁰⁻¹(𝄎β) = 𝄎α`.
|
uniformInducing_iff
theorem uniformInducing_iff :
∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] (f : α → β),
UniformInducing f ↔ Filter.comap (fun x => (f x.1, f x.2)) (uniformity β) = uniformity α
This theorem, `uniformInducing_iff`, states that for any two types `α` and `β` that have `UniformSpace` structures and for any function `f` from `α` to `β`, `f` is a Uniform Inducing function if and only if the preimage under `f` of the uniformity filter of `β` equals the uniformity filter of `α`. In more mathematical terms, the function `f` induces a uniform structure on `α` from `β` if and only if the uniform continuity condition holds, i.e., `(f x, f y)` is close in `β` whenever `(x, y)` is close in `α`.
More concisely: A function between two uniform spaces is a uniform inducing function if and only if the preimage of the uniformity filter on the codomain equals the uniformity filter on the domain.
|
comap_uniformity_of_spaced_out
theorem comap_uniformity_of_spaced_out :
∀ {β : Type v} [inst : UniformSpace β] {α : Type u_1} {f : α → β} {s : Set (β × β)},
s ∈ uniformity β →
(Pairwise fun x y => (f x, f y) ∉ s) → Filter.comap (Prod.map f f) (uniformity β) = Filter.principal idRel
This theorem states that if a function `f` mapping from a type `α` to a type `β` (within a uniform space) maps any two distinct elements to a pair of elements that are **not** related by a certain set `s` in the uniformity of `β`, then `f` induces a uniform structure with respect to the discrete uniformity on `α`. In other words, the preimage of the uniformity of `β` under the product map of `f` is the principal filter generated by the identity relation in the Cartesian product of `α` with itself. This means that `f` preserves the uniformity structure of `β` in a way that all distinct points in `α` are kept distinct in `β`.
More concisely: If a function from a uniform space to another maps distinct elements to unrelated elements under a given set, then it induces the discrete uniform structure on its domain.
|
isComplete_image_iff
theorem isComplete_image_iff :
∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {m : α → β} {s : Set α},
UniformInducing m → (IsComplete (m '' s) ↔ IsComplete s)
This theorem states that a set is complete if and only if its image under a uniform inducing map is complete. More specifically, for any two types `α` and `β` that have uniform space structures, any function `m` from `α` to `β`, and any set `s` of type `α`, if `m` is a uniform inducing function, then the set `s` is complete if and only if the image of `s` under `m` (denoted as `m '' s`) is complete. In mathematical terms, a set `s` is complete if every Cauchy filter `f` such that `s` belongs to `f`, has a limit in `s`.
More concisely: A set is complete if and only if its uniform image under a uniform inducing function is a complete subset.
|
UniformEmbedding.embedding
theorem UniformEmbedding.embedding :
∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
UniformEmbedding f → Embedding f
This theorem states that if 'f' is a function from one type 'α' to another type 'β', both equipped with a uniform space structure, and 'f' is a uniform embedding, then 'f' is also an embedding. In the context of topology and metric spaces, a uniform embedding means that the function 'f' not only maps 'α' to 'β' bijectively but also preserves the uniform structure, i.e., 'f' is a homeomorphism and it uniformly continues the given function. An embedding in this context means that 'f' is an injective function that induces a topology on 'α' that makes 'f' a homeomorphism onto its image.
More concisely: If 'f' is a uniform embedding of a uniform space ('α, dα) into another uniform space ('β, dβ), then 'f' is an embedding of ('α, dα) into ('β, dβ).
|
uniformEmbedding_comap
theorem uniformEmbedding_comap :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} [u : UniformSpace β], Function.Injective f → UniformEmbedding f := by
sorry
The theorem `uniformEmbedding_comap` states that for any types `α` and `β` and any function `f` from `α` to `β`, if `β` comes with a UniformSpace structure and the function `f` is injective, then `f` is a Uniform Embedding. In layman's terms, this theorem is saying if you have an injective function from one set to another, and the second set has a certain kind of mathematical structure called a Uniform Space, then that function preserves the structure in a certain way that qualifies it as a Uniform Embedding.
More concisely: If `α` is any type, `β` is a UniformSpace, and `f : α → β` is injective, then `f` is a Uniform Embedding.
|
UniformInducing.denseInducing
theorem UniformInducing.denseInducing :
∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
UniformInducing f → DenseRange f → DenseInducing f
The theorem `UniformInducing.denseInducing` states that for any two types `α` and `β` equipped with Uniform Space structures, and for any function `f` from `α` to `β`, if `f` is a uniform inducing function and has dense range, then `f` is a dense inducing function.
In more everyday language, this theorem is saying that if you have a function that transforms one set into another in a way that preserves a certain mathematical structure (uniformity), and the image of this function densely covers the target set, then this function not only induces a uniform structure but also induces a dense structure.
More concisely: If `f` is a uniform inducing function from a uniform space `(α, δα)` to another uniform space `(β, δβ)` with dense range, then `f` is a dense inducing function.
|
uniformEmbedding_iff
theorem uniformEmbedding_iff :
∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] (f : α → β),
UniformEmbedding f ↔ UniformInducing f ∧ Function.Injective f
The theorem `uniformEmbedding_iff` states that for all types `α` and `β` endowed with uniform spaces (denoted `[UniformSpace α]` and `[UniformSpace β]`), a function `f: α → β` is a uniform embedding if and only if it is both uniform inducing and injective. A function is uniform inducing if the topology on `α` induced by `f` is the same as the uniform space on `α`, and it is injective if for any two elements `a₁` and `a₂` in `α`, `f(a₁) = f(a₂)` implies that `a₁ = a₂`.
More concisely: A function between uniform spaces is a uniform embedding if and only if it is both uniformly continuous and injective.
|
uniformEmbedding_of_spaced_out
theorem uniformEmbedding_of_spaced_out :
∀ {β : Type v} [inst : UniformSpace β] {α : Type u_1} {f : α → β} {s : Set (β × β)},
s ∈ uniformity β → (Pairwise fun x y => (f x, f y) ∉ s) → UniformEmbedding f
The theorem `uniformEmbedding_of_spaced_out` states that for any given types `β` and `α`, with `β` having a uniform space structure, a mapping `f` from `α` to `β`, and a set `s` of pairs of elements of `β`, if `s` is an element of the uniformity of `β` and the pairs formed by applying `f` to distinct elements of `α` are not in `s` (that is, `f` sends any two distinct points to points that are not related by `s`), then `f` is a uniform embedding with respect to the discrete uniformity on `α`.
In other words, if a map sends different points in its domain to points in its codomain that do not satisfy a fixed relation that is present in the uniformity, then the map is a uniform embedding, maintaining the uniform structure.
More concisely: Given a uniform space `(β, Ξ)`, a map `f : α → β`, a set `s ∈ Ξ`, and distinct elements `x, y ∈ α` such that `(f x, f y) ∉ s`, then `f` is a uniform embedding from `(α, discrete)` to `(β, Ξ)`.
|
uniformContinuous_uniformly_extend
theorem uniformContinuous_uniformly_extend :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace α] [inst_1 : UniformSpace β]
[inst_2 : UniformSpace γ] {e : β → α} (h_e : UniformInducing e) (h_dense : DenseRange e) {f : β → γ},
UniformContinuous f → ∀ [inst_3 : CompleteSpace γ], UniformContinuous (⋯.extend f)
The theorem `uniformContinuous_uniformly_extend` states that for any three types `α`, `β`, and `γ` each equipped with a uniform space structure, and a function `e` mapping from `β` to `α` which induces a uniform structure, if the range of `e` is dense in `α`, then for any uniformly continuous function `f` from `β` to `γ`, provided `γ` is a complete space, the function `f` can be uniformly extended. This extended function is also uniformly continuous.
In other words, the theorem states that a uniformly continuous function defined on a dense subset of a space can be extended to a uniformly continuous function on the whole space, under the assumption that the codomain is a complete space.
More concisely: Given uniform spaces `α`, `β`, and `γ`, a dense subset `β` of `α`, a uniformly continuous function `f : β → γ` with complete codomain `γ`, there exists a uniformly continuous extension `g : α → γ` of `f`.
|
UniformInducing.uniformEmbedding
theorem UniformInducing.uniformEmbedding :
∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : T0Space α] {f : α → β},
UniformInducing f → UniformEmbedding f
This theorem states that for any two types `α` and `β` with a `UniformSpace` structure and where `α` also has a `T₀Space` structure, if a function `f` from `α` to `β` induces a uniform structure on `α`, then `f` is a uniform embedding. In other words, if `f` preserves the uniformity structure of `α` (making `α` a `UniformInducing` map), and `α` is a `T₀Space` (a topological space where for any two distinct points there is an open set containing one but not the other), then `f` is injective and thus a uniform embedding.
More concisely: If `α` is a T₀ space with a UniformSpace structure, and `f: α → β` is a uniformly continuous function that induces a uniform structure on `α`, then `f` is a uniform embedding (and thus injective).
|
completeSpace_congr
theorem completeSpace_congr :
∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {e : α ≃ β},
UniformEmbedding ⇑e → (CompleteSpace α ↔ CompleteSpace β)
This theorem states that, given two types `α` and `β` that are both uniform spaces, and given a bijection `e` from `α` to `β`, if this bijection is a uniform embedding, then `α` is a complete space if and only if `β` is a complete space. In other words, the completeness of a space is preserved under a uniform embedding. Here, a complete space is a space in which every Cauchy sequence (or Cauchy filter) converges.
More concisely: If `α` and `β` are uniform spaces with a uniformly bijective and uniformly continuous map `e` between them, then `α` and `β` are completeness-equivalent, i.e., they have the same Cauchy sequences.
|
UniformInducing.uniformContinuous_iff
theorem UniformInducing.uniformContinuous_iff :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
{f : α → β} {g : β → γ}, UniformInducing g → (UniformContinuous f ↔ UniformContinuous (g ∘ f))
The theorem `UniformInducing.uniformContinuous_iff` states that for any types `α`, `β`, and `γ` equipped with uniform spaces, and any functions `f : α → β` and `g : β → γ`, if `g` is a uniform inducing function, then `f` is uniformly continuous if and only if the composition of `g` and `f` (denoted `g ∘ f`) is uniformly continuous. In other words, the uniform continuity of `f` can be characterized through the uniform continuity of its composition with a uniform inducing function `g`.
More concisely: Given uniform spaces on types α, β, and γ, and uniformly inducing function g : β → γ, the function f : α → β is uniformly continuous if and only if the composition g ∘ f is uniformly continuous.
|
uniformInducing_iff'
theorem uniformInducing_iff' :
∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
UniformInducing f ↔ UniformContinuous f ∧ Filter.comap (Prod.map f f) (uniformity β) ≤ uniformity α
This theorem states that for any two types `α` and `β` both equipped with a uniform space structure and any function `f` from `α` to `β`, `f` is a uniform inducing function if and only if `f` is uniformly continuous and the pre-image filter (also known as the pullback or comap) of the filter generated by `f` acting on each element of the product of `β` itself, when taken under the uniformity of `β`, is less than or equal to the uniformity of `α`. In simpler terms, this theorem is about the conditions under which a function between two uniform spaces preserves the uniformity structure.
More concisely: A function between two uniform spaces is a uniform inducing function if and only if it is uniformly continuous and the pre-image filter of its filter generated on the product under the uniformity of the target space is less than or equal to the uniformity of the domain.
|