UniformSpace.Completion.induction_on₂
theorem UniformSpace.Completion.induction_on₂ :
∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β]
{p : UniformSpace.Completion α → UniformSpace.Completion β → Prop} (a : UniformSpace.Completion α)
(b : UniformSpace.Completion β), IsClosed {x | p x.1 x.2} → (∀ (a : α) (b : β), p (↑α a) (↑β b)) → p a b
This theorem states that for any two types `α` and `β` both equipped with a uniform space structure, and any property `p` relating elements of the Hausdorff completions of `α` and `β`, if the set of pairs `(x, y)` such that `p x y` holds is closed, and `p` holds for all pairs `(a, b)` of elements of `α` and `β` respectively, then `p` also holds for any pair `(a, b)` of elements in the Hausdorff completions of `α` and `β`. In simpler terms, the theorem indicates a method to extend properties from original spaces to their completions, under certain conditions.
More concisely: Given types `α` and `β` with uniform structures, and a property `p` on their Hausdorff completions such that the set of pairs `(x, y)` with `p x y` closed and `p ab` for all `a ∈ α` and `b ∈ β` implies `p xy` for any `x ∈ α↓` and `y ∈ β↓`, where `↓` denotes the Hausdorff completion.
|
CauchyFilter.uniformInducing_pureCauchy
theorem CauchyFilter.uniformInducing_pureCauchy :
∀ {α : Type u} [inst : UniformSpace α], UniformInducing CauchyFilter.pureCauchy
The theorem `CauchyFilter.uniformInducing_pureCauchy` states that for every type `α` that has a `UniformSpace` structure, the function `CauchyFilter.pureCauchy` is uniformly inducing. In other words, `CauchyFilter.pureCauchy` has the property that the preimage of a uniformity on the completion of `α` (i.e., `CauchyFilter α`) under this function is equal to the uniformity on `α`. This function embeds `α` into its completion, the space of Cauchy filters on `α`, and ensures that uniform properties are preserved under this embedding.
More concisely: For any type `α` with a `UniformSpace` structure, the function `CauchyFilter.pureCauchy` is a uniformly inducing map from `α` to its completion `CauchyFilter α`.
|
UniformSpace.Completion.comap_coe_eq_uniformity
theorem UniformSpace.Completion.comap_coe_eq_uniformity :
∀ (α : Type u_1) [inst : UniformSpace α],
Filter.comap (fun p => (↑α p.1, ↑α p.2)) (uniformity (UniformSpace.Completion α)) = uniformity α
This theorem states that for any type `α` equipped with a uniform space structure, the filter obtained by taking the preimage (comap) through the function that maps each pair of elements in `α` to a pair in the completion of `α` (using the canonical embedding `↑α`) applied to the uniformity of the completion of `α`, is equal to the original uniformity of `α`. In other words, the uniformity filter on the completion of `α` under this mapping corresponds exactly to the original uniformity filter of `α`. This theorem is essential in the analysis of uniform spaces and their completions, and provides a link between the original space and its completion.
More concisely: For any uniform space `(α, Δ)`, the filter on `α × α` obtained by composing the diagonal map with the canonical embedding of `α` into its completion, is equal to the original uniformity filter `Δ`.
|
UniformSpace.Completion.map_coe
theorem UniformSpace.Completion.map_coe :
∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {f : α → β},
UniformContinuous f → ∀ (a : α), UniformSpace.Completion.map f (↑α a) = ↑β (f a)
This theorem states that, for any two types `α` and `β` equipped with uniform spaces and any function `f` from `α` to `β` that is uniformly continuous, then for any element `a` of `α`, the completion of the map `f` at the completion of `a` is equal to the completion of `f(a)`. In other words, if we first apply the function `f` to an element and then complete it, it is the same as if we first complete the element and then apply the completed function.
More concisely: For any uniformly continuous function `f` from complete uniform space `α` to complete uniform space `β`, the completion of `f` at a point `a` in `α` is equal to the completion of `f(a)` in `β`.
|
UniformSpace.Completion.uniformContinuous_extension₂
theorem UniformSpace.Completion.uniformContinuous_extension₂ :
∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {γ : Type u_3}
[inst_2 : UniformSpace γ] (f : α → β → γ) [inst_3 : CompleteSpace γ],
UniformContinuous₂ (UniformSpace.Completion.extension₂ f)
The theorem `UniformSpace.Completion.uniformContinuous_extension₂` states that for any three types `α`, `β`, and `γ` equipped with uniform spaces, any function `f` from `α` to `β` to `γ`, and given that `γ` is a complete space, then the extension of the function `f` to the completion of `α` and `β` is uniformly continuous. In mathematical terms, if `f : α → β → γ` is a function with `α`, `β`, `γ` being uniform spaces and `γ` is complete, then the function `f' : UniformSpace.Completion α → UniformSpace.Completion β → γ`, which extends `f`, is uniformly continuous.
More concisely: Given functions `f : α → β → γ` between complete uniform spaces `α`, `β`, and a complete uniform space `γ`, the extension `f' : UniformSpace.Completion α → UniformSpace.Completion β → γ` of `f` is uniformly continuous.
|
UniformSpace.Completion.continuous_map
theorem UniformSpace.Completion.continuous_map :
∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {f : α → β},
Continuous (UniformSpace.Completion.map f)
The theorem `UniformSpace.Completion.continuous_map` states that for all types `α` and `β` which are equipped with a `UniformSpace` structure, and for any function `f` from `α` to `β`, the map `UniformSpace.Completion.map f` is continuous. In other words, if we take a function from one `UniformSpace` to another and apply the completion functor to it, the resulting function is guaranteed to be continuous. Here, continuity of a function means that the inverse image of any open set in the co-domain is open in the domain. In the context of uniform spaces (which are a generalization of metric spaces), this theorem ensures that we can work with complete spaces without loss of continuity.
More concisely: The completion of a continuous function between uniform spaces is a continuous function.
|
UniformSpace.Completion.continuous_coe
theorem UniformSpace.Completion.continuous_coe : ∀ (α : Type u_1) [inst : UniformSpace α], Continuous ↑α
This theorem states that for any type `α` equipped with a uniform space structure, the natural embedding from `α` into its completion is continuous. In other words, given any uniform space, the function that maps each element to its corresponding element in the complete space is a continuous function. This is a key property in the theory of uniform spaces and is significant in the study of completeness and limit processes within these spaces.
More concisely: For any uniform space `(α, δ)`, the natural embedding `α ⊆ Ⓐ(α)` is a continuous function with respect to the uniform structures `δ` and the standard uniform structure on `Ⓐ(α)`. (Here, `Ⓐ(α)` denotes the completion of `α`.)
|
CauchyFilter.denseRange_pureCauchy
theorem CauchyFilter.denseRange_pureCauchy :
∀ {α : Type u} [inst : UniformSpace α], DenseRange CauchyFilter.pureCauchy
The theorem `CauchyFilter.denseRange_pureCauchy` states that for any type `α` equipped with a uniform space structure, the function `pureCauchy` from `α` to its completion `CauchyFilter α` has a dense range. In other words, the image (or range) of any element of `α` under the `pureCauchy` function is a dense subset of the Cauchy completion of `α`. This implies that any point in the completion can be approximated arbitrarily closely by images under `pureCauchy` of points in `α`.
More concisely: The range of the `pureCauchy` function from a uniform space `α` to its Cauchy completion `CauchyFilter α` is dense.
|
UniformSpace.Completion.map_comp
theorem UniformSpace.Completion.map_comp :
∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {γ : Type u_3}
[inst_2 : UniformSpace γ] {g : β → γ} {f : α → β},
UniformContinuous g →
UniformContinuous f →
UniformSpace.Completion.map g ∘ UniformSpace.Completion.map f = UniformSpace.Completion.map (g ∘ f)
The theorem `UniformSpace.Completion.map_comp` states that for all types `α`, `β`, and `γ` equipped with uniform spaces, given two functions `g : β → γ` and `f : α → β`, if both `g` and `f` are uniformly continuous, then the composition of the mappings of `g` and `f` in the completion spaces is equal to the mapping in the completion space of the composition of `g` and `f`. In other words, if we first map from `α` to `β` using `f` and then from `β` to `γ` using `g`, both in the completion spaces, it's the same as if we first compose `g` and `f` and then map from `α` to `γ` in the completion space. This is a property of uniform continuity in the context of completion spaces, which are spaces that include all limits necessary to complete a given space.
More concisely: Given uniformly continuous functions `f : α → β` and `g : β → γ` between completion spaces, `(g ∘ f) hat = hat(g ∘ f)`, where `hat` denotes the completion mapping.
|
UniformSpace.Completion.denseInducing_coe
theorem UniformSpace.Completion.denseInducing_coe : ∀ {α : Type u_1} [inst : UniformSpace α], DenseInducing ↑α := by
sorry
This theorem states that for any type `α` that carries a `UniformSpace` structure, the coercive function from that type into its completion induces a dense subset. In simpler terms, any point in the completion of the uniform space can be approximated as closely as desired by a point from the original space, making the original space "dense" within its completion.
More concisely: For any uniform space `(α, δ)`, the coercion map from `α` to its completion `(COMP α, δ')` is a continuous surjection with dense source, i.e., every point in `COMP α` can be approximated by a sequence of points in `α`.
|
UniformSpace.Completion.uniformContinuous_map
theorem UniformSpace.Completion.uniformContinuous_map :
∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {f : α → β},
UniformContinuous (UniformSpace.Completion.map f)
The theorem `UniformSpace.Completion.uniformContinuous_map` states that for any two types `α` and `β` equipped with a uniform space structure, and for any function `f` from `α` to `β`, the completion map of `f` (represented as `UniformSpace.Completion.map f`) is uniformly continuous. In other words, if `x` and `y` are sufficiently close points in the completion of `α`, then their images under the `f` completion map in the completion of `β` are also close, regardless of the specific locations of `x` and `y` in the completion of `α`.
More concisely: Given uniform spaces (α, dα) and (β, dβ), and a uniformly continuous function f : α → β, the completion map UniformSpace.Completion.map f is uniformly continuous from the completion of (α, dα) to the completion of (β, dβ).
|
UniformSpace.Completion.continuous_extension
theorem UniformSpace.Completion.continuous_extension :
∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {f : α → β}
[inst_2 : CompleteSpace β], Continuous (UniformSpace.Completion.extension f)
This theorem states that, for any types `α` and `β` that are equipped with uniform space structures, and for any function `f` from `α` to `β`, if `β` is a complete space, then the extension of the function `f` to the completion of `α` is continuous. This extension, called `UniformSpace.Completion.extension f`, is defined for any map `f`, although it returns an arbitrary constant value if `f` is not uniformly continuous.
More concisely: If `α` and `β` are uniform spaces with `β` complete, and `f : α → β` is a uniformly continuous function, then the extension `UniformSpace.Completion.extension f` of `f` to the completions of `α` and `β` is a continuous function.
|
UniformSpace.Completion.denseRange_coe
theorem UniformSpace.Completion.denseRange_coe : ∀ {α : Type u_1} [inst : UniformSpace α], DenseRange ↑α
This theorem states that for any type `α` equipped with a Uniform Space structure, the coercion function from `α` to its completion (denoted by `↑α`) has a dense range. In other words, the image (or range) of the original set `α` under the coercion function is a dense subset of the completion of `α`. In terms of topology, this means that every point in the completion of `α` can be approximated as closely as desired by points from `α`.
More concisely: For any uniform space `(α, τ)`, the coercion function from `α` to its completion `(↑α, τ↑)` has a dense range.
|
UniformSpace.Completion.ext'
theorem UniformSpace.Completion.ext' :
∀ {α : Type u_1} [inst : UniformSpace α] {Y : Type u_4} [inst_1 : TopologicalSpace Y] [inst_2 : T2Space Y]
{f g : UniformSpace.Completion α → Y},
Continuous f → Continuous g → (∀ (a : α), f (↑α a) = g (↑α a)) → ∀ (a : UniformSpace.Completion α), f a = g a
This theorem states that for any type `α` that is a uniform space and any type `Y` that is a topological space and a T2 space, if `f` and `g` are two functions from the Hausdorff (T2) completion of `α` to `Y` and both are continuous, then if `f` and `g` agree on the elements of `α` (i.e. `f` applied to any element of `α` is the same as `g` applied to the same element), they agree on all elements of the Hausdorff completion of `α`. That is, for any element `a` of the Hausdorff completion of `α`, the value of `f` at `a` is equal to the value of `g` at `a`. This is a universal property of the completion of a uniform space.
More concisely: Given a uniform space `α`, a T2 topological space `Y`, and continuous functions `f` and `g` from the Hausdorff completion of `α` to `Y` that agree on `α`, they agree on all elements of the Hausdorff completion of `α`.
|
CauchyFilter.uniformEmbedding_pureCauchy
theorem CauchyFilter.uniformEmbedding_pureCauchy :
∀ {α : Type u} [inst : UniformSpace α], UniformEmbedding CauchyFilter.pureCauchy
The theorem `CauchyFilter.uniformEmbedding_pureCauchy` states that for every type `α` equipped with a uniform space structure, the function `pureCauchy` which embeds `α` into its completion `CauchyFilter α` is a uniform embedding. A uniform embedding is a function between two uniform spaces that preserves the uniformity structure, meaning that it is injective and the topology induced by the uniform structure on the domain is the same as the subspace topology from the codomain.
More concisely: The `pureCauchy` function, which embeds a uniform space `α` into its completion `CauchyFilter α`, is a uniform embedding.
|
UniformSpace.Completion.uniformContinuous_coe
theorem UniformSpace.Completion.uniformContinuous_coe :
∀ (α : Type u_1) [inst : UniformSpace α], UniformContinuous ↑α
This theorem states that for any type `α` accompanied by a `UniformSpace` structure, the coercion function from `α` to its completion is uniformly continuous. In other words, if `x` and `y` are close enough in `α`, then their images under the coercion function are also close in the completion of `α`, regardless of their specific locations in `α`. This property holds for all elements in the type `α`.
More concisely: For any uniform space `(α, δ)` with a coercion to its completion `C α`, the coercion function is uniformly continuous, i.e., for all `x, y ∈ α` with `δ(x, y)` small enough, `δ(x, y) ≤ ε` implies `∥coe α x - coe α y∥ ≤ ε`, where `coe α : α → C α` is the coercion function and `∥.∥` denotes the metric on the completion `C α`.
|
UniformSpace.Completion.uniformEmbedding_coe
theorem UniformSpace.Completion.uniformEmbedding_coe :
∀ (α : Type u_1) [inst : UniformSpace α] [inst_1 : T0Space α], UniformEmbedding ↑α
The theorem `UniformSpace.Completion.uniformEmbedding_coe` states that for any type `α` that has a uniform space structure and a T0 space structure, the canonical embedding of `α` into its completion is a uniform embedding. In the language of mathematics, given any topological space `α` that is both uniform and T0, the function that maps each point in `α` to the corresponding point in the completion of `α` is a uniform embedding, which preserves all the uniform properties of the space.
More concisely: The canonical embedding of a uniform and T0 space into its completion is a uniform embedding.
|
UniformSpace.Completion.extension_coe
theorem UniformSpace.Completion.extension_coe :
∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {f : α → β} [inst_2 : T0Space β],
UniformContinuous f → ∀ (a : α), UniformSpace.Completion.extension f (↑α a) = f a
This theorem states that for any types `α` and `β` which are uniform spaces, and for any function `f` from `α` to `β` which is uniformly continuous, then the extension of `f` to the completion of `α` evaluated at any point `a` of `α` (notated as `↑α a`) is equal to `f` evaluated at `a`. This essentially means that when `f` is uniformly continuous, its extension to the completion of `α` acts exactly like `f` on the original points of `α`. Furthermore, the theorem assumes that `β` is a T0 space, which is a separation axiom in topology that says for any two distinct points in `β`, there exists an open set containing one of them but not the other.
More concisely: If `α` and `β` are uniform spaces, `f : α → β` is uniformly continuous, and `β` is T0, then for any `a : α`, `f (↑α a) = f a`.
|
UniformSpace.Completion.continuous_map₂
theorem UniformSpace.Completion.continuous_map₂ :
∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {γ : Type u_3}
[inst_2 : UniformSpace γ] {δ : Type u_4} [inst_3 : TopologicalSpace δ] {f : α → β → γ}
{a : δ → UniformSpace.Completion α} {b : δ → UniformSpace.Completion β},
Continuous a → Continuous b → Continuous fun d => UniformSpace.Completion.map₂ f (a d) (b d)
The theorem `UniformSpace.Completion.continuous_map₂` states that for any three types `α`, `β`, and `γ` each equipped with a uniform structure, and a fourth type `δ` with a topological structure, given a continuous function `a: δ → UniformSpace.Completion α` and a continuous function `b: δ → UniformSpace.Completion β`, the mapping function `f: α → β → γ` can be lifted to a function on the completions `UniformSpace.Completion.map₂ f (a d) (b d)` and this function is continuous. In other words, the lifted function `f` is a continuous function when operating on the Hausdorff completions of `α` and `β`.
More concisely: Given continuous functions from a Hausdorff space with uniform structure to the completions of two uniform spaces, their composition can be lifted to a continuous function between the completions.
|
UniformSpace.Completion.induction_on
theorem UniformSpace.Completion.induction_on :
∀ {α : Type u_1} [inst : UniformSpace α] {p : UniformSpace.Completion α → Prop} (a : UniformSpace.Completion α),
IsClosed {a | p a} → (∀ (a : α), p (↑α a)) → p a
This theorem, called `UniformSpace.Completion.induction_on`, states that for any type `α` with a uniform space structure, a property `p`, and an element `a` of the completion of `α`, if the set of all `a` for which `p a` holds is closed, and `p` holds for all elements of `α`, then `p` also holds for `a`. In other words, it provides an induction principle for proving properties about the elements of the completion of a uniform space, given that these properties hold for the elements of the original space and are preserved under taking limits (since being closed means containing all limit points).
More concisely: If `α` is a uniform space with property `p` holding for all elements of `α` and the set of all completion elements `a` with `p a` is closed, then `p` holds for all completion elements `a`.
|
UniformSpace.Completion.induction_on₃
theorem UniformSpace.Completion.induction_on₃ :
∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {γ : Type u_3}
[inst_2 : UniformSpace γ]
{p : UniformSpace.Completion α → UniformSpace.Completion β → UniformSpace.Completion γ → Prop}
(a : UniformSpace.Completion α) (b : UniformSpace.Completion β) (c : UniformSpace.Completion γ),
IsClosed {x | p x.1 x.2.1 x.2.2} → (∀ (a : α) (b : β) (c : γ), p (↑α a) (↑β b) (↑γ c)) → p a b c
The theorem `UniformSpace.Completion.induction_on₃` states that for any three types `α`, `β`, and `γ` equipped with a uniform space structure, and for any predicate `p` defined on the Hausdorff completions of `α`, `β`, and `γ`, if the set of triples in the product space of the completions on which `p` holds is closed, and `p` holds for any triple of points in the original spaces `α`, `β`, and `γ`, then `p` also holds for any triple of points in the completions `UniformSpace.Completion α`, `UniformSpace.Completion β`, and `UniformSpace.Completion γ`. This theorem expresses a property of induction on the completions of uniform spaces.
More concisely: If the set of triples in the product of the Hausdorff completions of uniform spaces `α`, `β`, and `γ` where a predicate `p` holds is closed and `p` holds for all triples in the original spaces, then `p` holds for all triples in the completions.
|