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 UniformSpace.Completion.instNorm (E : Type u_1) [UniformSpace E] [Norm E] : Norm (Completion E)

Equations

• UniformSpace.Completion.instNorm E = { norm := UniformSpace.Completion.extension norm }

@[simp]

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

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

Equations

• UniformSpace.Completion.instNormedAddCommGroup E = NormedAddCommGroup.mk ⋯

@[simp]

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