mathlib3 documentation

analysis.normed.group.completion

Completion of a normed group #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Tags #

normed group, completion

@[protected, instance]

noncomputable def uniform_space.completion.has_norm (E : Type u_1) [uniform_space E] [has_norm E] :

has_norm (uniform_space.completion E)

Equations

uniform_space.completion.has_norm E = {norm := uniform_space.completion.extension has_norm.norm}

@[simp]

theorem uniform_space.completion.norm_coe {E : Type u_1} [seminormed_add_comm_group E] (x : E) :

‖↑x‖ = ‖x‖

@[protected, instance]

noncomputable def uniform_space.completion.normed_add_comm_group (E : Type u_1) [seminormed_add_comm_group E] :

normed_add_comm_group (uniform_space.completion E)

Equations

uniform_space.completion.normed_add_comm_group E = {to_has_norm := uniform_space.completion.has_norm E seminormed_add_comm_group.to_has_norm, to_add_comm_group := {add := add_comm_group.add uniform_space.completion.add_comm_group, add_assoc := _, zero := add_comm_group.zero uniform_space.completion.add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul uniform_space.completion.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg uniform_space.completion.add_comm_group, sub := add_comm_group.sub uniform_space.completion.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul uniform_space.completion.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}, to_metric_space := {to_pseudo_metric_space := metric_space.to_pseudo_metric_space uniform_space.completion.metric_space, eq_of_dist_eq_zero := _}, dist_eq := _}