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

@[implicit_reducible]

noncomputable 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‖

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[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‖ₑ