AbstractCompletion.continuous_extend
theorem AbstractCompletion.continuous_extend :
∀ {α : Type u_1} [inst : UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [inst_1 : UniformSpace β]
{f : α → β} [inst_2 : CompleteSpace β], Continuous (pkg.extend f)
The theorem `AbstractCompletion.continuous_extend` states that for any types `α` and `β` equipped with a uniform space structure, a completion `pkg` of `α`, and a function `f` from `α` to `β`, if `β` is a complete space, then the extension of the function `f` to the completed space `pkg.space` is continuous. Here, the extension of `f` is achieved by the `AbstractCompletion.extend` function.
More concisely: Given a uniform space `α`, a completion `pkg.space` of `α`, a function `f : α → β` where `β` is a complete space, the theorem asserts that the extension of `f` to `pkg.space` via `AbstractCompletion.extend` is a continuous function.
|
AbstractCompletion.continuous_map
theorem AbstractCompletion.continuous_map :
∀ {α : Type u_1} [inst : UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [inst_1 : UniformSpace β]
(pkg' : AbstractCompletion β) (f : α → β), Continuous (pkg.map pkg' f)
The theorem `AbstractCompletion.continuous_map` asserts that for any two types `α` and `β` equipped with Uniform Spaces, and their respective abstract completions `pkg` and `pkg'`, if there exists a function `f` from `α` to `β`, then the function obtained by mapping `f` to these completions, which is `AbstractCompletion.map pkg pkg' f`, is continuous. In other words, this theorem is about the continuity preservation property of the process of lifting maps to completions in the context of abstract completions and Uniform Spaces.
More concisely: Given types `α` and `β` with Uniform Spaces structures, and functions `f: α → β`, the function `AbstractCompletion.map` preserves continuity: `AbstractCompletion.map ℵ ℵ' f` is continuous, where `ℵ` and `ℵ'` are the respective abstract completions.
|
AbstractCompletion.dense
theorem AbstractCompletion.dense :
∀ {α : Type u} [inst : UniformSpace α] (self : AbstractCompletion α), DenseRange self.coe
This theorem states that for any `α` that is a type equipped with a uniform space structure, and for any abstract completion of `α`, the mapping into the completion (given by `self.coe`) has a dense range. In other words, the image of the mapping `self.coe` forms a dense subset in the completion space. In terms of topology, this means that every open set in the completion space contains a point from the image of `self.coe`.
More concisely: For any uniform space `α` and its completion, the evaluation map from `α` to its completion has a dense range.
|
AbstractCompletion.uniformContinuous_extend
theorem AbstractCompletion.uniformContinuous_extend :
∀ {α : Type u_1} [inst : UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [inst_1 : UniformSpace β]
{f : α → β} [inst_2 : CompleteSpace β], UniformContinuous (pkg.extend f)
The theorem `AbstractCompletion.uniformContinuous_extend` asserts that for any types `α` and `β` equipped with a uniform space structure, any abstract completion `pkg` of `α`, and any function `f : α → β`, if `β` is a complete space, then the extension of the function `f` to the completion `pkg.space` is uniformly continuous. That is, regardless of where two points in `pkg.space` are located, if they are sufficiently close to each other, then their images under the extension of `f` are also close to each other.
More concisely: Given types `α` and `β` with uniform structures, an abstract completion `pkg` of `α`, and a function `f : α → β` with complete domain `β`, the extension of `f` to `pkg.space` is uniformly continuous.
|
AbstractCompletion.extend_coe
theorem AbstractCompletion.extend_coe :
∀ {α : Type u_1} [inst : UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [inst_1 : UniformSpace β]
{f : α → β} [inst_2 : T2Space β], UniformContinuous f → ∀ (a : α), pkg.extend f (pkg.coe a) = f a
The theorem `AbstractCompletion.extend_coe` states that for any types `α` and `β` with respective uniform spaces, any uniform continuous function `f` from `α` to `β`, and any element `a` of `α`, if we extend the function `f` to the completion of `α` and apply it to the embedding of `a` in the completion, we get the same result as applying `f` to `a` directly. This theorem ensures that the extension of `f` to the completion is consistent with the original function `f` on the original space `α`. This holds under the assumption that `β` is a Hausdorff space (T2 space), which guarantees unique limits in `β`.
More concisely: For any Hausdorff spaces `α` and `β`, uniformly continuous `f : α → β`, and `a : α`, the extension of `f` to the completions of `α` and `β` satisfy `f(completion_of_a) = completion_of(f a)`.
|
AbstractCompletion.funext
theorem AbstractCompletion.funext :
∀ {α : Type u_1} [inst : UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [inst_1 : TopologicalSpace β]
[inst_2 : T2Space β] {f g : pkg.space → β},
Continuous f → Continuous g → (∀ (a : α), f (pkg.coe a) = g (pkg.coe a)) → f = g
This theorem states that for any type `α` that is a Uniform Space and another type `β` which is a topological space with `T2Space` properties (i.e., a Hausdorff space), and given two continuous functions `f` and `g` from the space of abstract completion of `α` to `β`, if they agree on each point `a` of `α` (i.e., `f (pkg.coe a)` is equal to `g (pkg.coe a)` for all `a` in `α`), then the functions `f` and `g` are identical. This is essentially an extensionality property of functions in the context of topological and uniform spaces.
More concisely: If `α` is a Uniform Space and `β` is a T2Space, and `f` and `g` are continuous functions from the completion of `α` to `β` that agree on all points in `α`, then `f` and `g` are equal.
|
AbstractCompletion.uniformInducing
theorem AbstractCompletion.uniformInducing :
∀ {α : Type u} [inst : UniformSpace α] (self : AbstractCompletion α), UniformInducing self.coe
This theorem states that for any type `α` equipped with a UniformSpace structure, the map (`self.coe`) into its abstract completion (constructed via `self : AbstractCompletion α`) is uniform inducing. In the context of topology, a function is said to be uniform inducing if the topology on the domain induced by the function's uniform structure is the same as the original topology of the domain. In simple terms, the theorem asserts that the process of completing a uniform space preserves the uniformity of the original space.
More concisely: For any uniform space `α`, the natural map from `α` to its completion is uniformly continuous.
|
AbstractCompletion.separation
theorem AbstractCompletion.separation :
∀ {α : Type u} [inst : UniformSpace α] (self : AbstractCompletion α), T0Space self.space
This theorem states that for any type `α` that is equipped with a uniform space structure, the abstract completion of `α` yields a T₀ space. In the context of topology, a T₀ space is a topological space where for any two distinct points, there is a neighborhood of one that does not contain the other. This property is also known as Kolmogorov separation. Therefore, this theorem is essentially about the separation properties of the abstract completion of a given topological space.
More concisely: The abstract completion of any uniform space is a T0 space.
|
AbstractCompletion.uniformContinuous_coe
theorem AbstractCompletion.uniformContinuous_coe :
∀ {α : Type u_1} [inst : UniformSpace α] (pkg : AbstractCompletion α), UniformContinuous pkg.coe
This theorem states that for any type `α` equipped with a uniform space structure and any abstract completion `pkg` of `α`, the canonical mapping (denoted by `pkg.coe`) from `α` to the abstract completion `pkg` is uniformly continuous. In mathematical terms, this means that for any two points `x` and `y` in `α` that are sufficiently close to each other, their images under `pkg.coe` (i.e., `pkg.coe(x)` and `pkg.coe(y)`) are also close to each other, regardless of the specific locations of `x` and `y` in `α`.
More concisely: For any uniform space `(α, δ)` and its abstract completion `(COMP α, δ')`, the canonical map `α →* COMP α` is a uniformly continuous function.
|
AbstractCompletion.complete
theorem AbstractCompletion.complete :
∀ {α : Type u} [inst : UniformSpace α] (self : AbstractCompletion α), CompleteSpace self.space
This theorem establishes the completeness of an abstract completion of a given uniform space. In the context of the theorem, for any type `α` that is equipped with a uniform space structure, this theorem guarantees that the associated `AbstractCompletion` of `α` is a complete space. In mathematical terms, this essentially means that every Cauchy sequence in the `AbstractCompletion` space has a limit in that same space.
More concisely: Given a type `α` with a uniform space structure, the associated `AbstractCompletion` of `α` is a complete uniform space.
|
AbstractCompletion.uniformContinuous_compare
theorem AbstractCompletion.uniformContinuous_compare :
∀ {α : Type u_1} [inst : UniformSpace α] (pkg pkg' : AbstractCompletion α), UniformContinuous (pkg.compare pkg')
The theorem `AbstractCompletion.uniformContinuous_compare` states that for any type `α` that is equipped with a uniform space structure, and any two abstract completions `pkg` and `pkg'` of that uniform space, the comparison map between these two completions is uniformly continuous. In other words, if two points in the space of the first abstract completion are sufficiently close to each other, then their images under the comparison map in the space of the second abstract completion are also close to each other, regardless of their location in the original uniform space.
More concisely: Given two abstract completions of a uniform space, the comparison map between them is uniformly continuous.
|