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

Equations

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

@[simp]

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

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

Equations

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