UniformSpace.Completion.coe_mul
theorem UniformSpace.Completion.coe_mul :
∀ {α : Type u_1} [inst : Ring α] [inst_1 : UniformSpace α] [inst_2 : TopologicalRing α] (a b : α),
↑α (a * b) = ↑α a * ↑α b
This theorem states that for any type `α` that is a Ring and a Topological Ring with a Uniform Space structure, the completion operation respects multiplication. In other words, for any two elements `a` and `b` of `α`, the completion of the product `a * b` is the same as the product of the completions of `a` and `b`. This theorem formalizes one of the essential properties of complete metric spaces that are also rings.
More concisely: For any commutative ring `α` with a uniform space structure, the completion operation is multiplicative, i.e., `∫(a * b) dμ = ∫(a) dμ * ∫(b) dμ` for any `a, b` in `α`, where `∫` denotes the completion and `μ` is the compatible measure on the uniform space.
|
UniformSpace.Completion.continuous_mul
theorem UniformSpace.Completion.continuous_mul :
∀ {α : Type u_1} [inst : Ring α] [inst_1 : UniformSpace α] [inst_2 : TopologicalRing α]
[inst_3 : UniformAddGroup α], Continuous fun p => p.1 * p.2
This theorem states that for any type `α` that has a ring structure, a uniform space structure, is a topological ring, and a uniform add group, the multiplication operation, which takes a pair of elements and returns their product, is continuous. This means that for any small change in the input values, there is a correspondingly small change in the output value. This property is crucial for many mathematical constructs involving limits, derivatives, and integrals, among others.
More concisely: For any type `α` endowed with a ring structure, a uniform space structure making it a topological ring, and a uniform add group, the multiplication operation is continuous.
|
UniformSpace.Completion.Continuous.mul
theorem UniformSpace.Completion.Continuous.mul :
∀ {α : Type u_1} [inst : Ring α] [inst_1 : UniformSpace α] [inst_2 : TopologicalRing α] [inst_3 : UniformAddGroup α]
{β : Type u_2} [inst_4 : TopologicalSpace β] {f g : β → UniformSpace.Completion α},
Continuous f → Continuous g → Continuous fun b => f b * g b
This theorem states that for any type `α` which has a ring structure, a uniform space structure, a topological ring structure, and is a uniform additive group, and for any other type `β` which has a topological space structure, if `f` and `g` are continuous functions from `β` to the Hausdorff completion of `α`, then the function which maps an element `b` in `β` to the product of `f(b)` and `g(b)` in the Hausdorff completion of `α` is also continuous. In other words, the product of two continuous functions remains continuous in the context of the Hausdorff completion of a topological ring when the ring is also a uniform space and a uniform additive group.
More concisely: If `α` is a topological ring and uniform additive group, `β` is a topological space, and `f` and `g` are continuous functions from `β` to the Hausdorff completion of `α`, then the function that maps `b` to `f(b)` \* `g(b)` in the Hausdorff completion of `α` is also continuous.
|