Mathlib.Topology.Algebra.GroupCompletion._auxLemma.3
theorem Mathlib.Topology.Algebra.GroupCompletion._auxLemma.3 :
∀ {α : Type u_3} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : UniformAddGroup α] (a b : α),
↑α a + ↑α b = ↑α (a + b)
This theorem, from the Mathlib.Topology.Algebra.GroupCompletion module, states that for any type `α` that has a Uniform Space structure, an Addition Group structure, and a Uniform Addition Group structure, the sum of the embeddings of two elements `a` and `b` from `α` is equal to the embedding of the sum of these two elements. In simpler terms, this is stating that the operation of embedding preserves the addition operation in the space `α`.
More concisely: For any type `α` with a Uniform Space, Addition Group, and Uniform Addition Group structure, the embedding function maps the sum of any two elements to the sum of their embeddings.
|
UniformSpace.Completion.coe_zero
theorem UniformSpace.Completion.coe_zero : ∀ {α : Type u_3} [inst : UniformSpace α] [inst_1 : Zero α], ↑α 0 = 0 := by
sorry
This theorem states that for any type `α` that is a uniform space and has a zero element, the completion of the space maps the zero element of `α` to the zero element of the completion. In mathematics terms, if `α` is a uniform space and `0` is a zero element in `α`, the embedding of `α` into its completion sends `0` to `0`.
More concisely: If `(α, d)` is a uniform space with a zero element `0`, then the completion `(Ⓐα, ∥.∥)` of `α` contains the zero element `ℝ⁇0` such that the embedding `α ��射游 Ⓐα` sends `0` to `ℝ⁇0`.
|
UniformSpace.Completion.coe_add
theorem UniformSpace.Completion.coe_add :
∀ {α : Type u_3} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : UniformAddGroup α] (a b : α),
↑α (a + b) = ↑α a + ↑α b
This theorem, `UniformSpace.Completion.coe_add`, states that for any type `α` that is a uniform space, an add group, and a uniform add group, the completion of the sum of two elements `a` and `b` of type `α` is equal to the sum of the completions of `a` and `b`. In other words, the operation of taking the completion in this context distributes over addition. This is a property of uniform spaces that also have a group structure where the group operation is compatible with the uniform structure.
More concisely: For any uniform add group `α`, the completion of the sum of two elements `a` and `b` is equal to the sum of their completions.
|