Completion of a normed group

In this file we prove that the completion of a (semi)normed group is a normed group.

Tags

normed group, completion

@[instance_reducible]

noncomputable instance UniformSpace.Completion.instNorm (E : Type u_1) [UniformSpace E] [Norm E] : Norm (Completion E)

@[simp]

theorem UniformSpace.Completion.norm_coe {E : Type u_2} [SeminormedAddCommGroup E] (x : E) : ‖↑x‖ = ‖x‖

@[instance_reducible]

noncomputable instance UniformSpace.Completion.instNormedAddCommGroup (E : Type u_1) [SeminormedAddCommGroup E] : NormedAddCommGroup (Completion E)

@[simp]

theorem UniformSpace.Completion.nnnorm_coe {E : Type u_2} [SeminormedAddCommGroup E] (x : E) : ‖↑x‖₊ = ‖x‖₊

@[simp]

theorem UniformSpace.Completion.enorm_coe {E : Type u_2} [SeminormedAddCommGroup E] (x : E) : ‖↑x‖ₑ = ‖x‖ₑ