mathlib documentation

topology.algebra.normed_group

Completion of normed groups #

In this file we show that the completion of a normed group is naturally a normed group.

Main declaration #

uniform_space.completion.normed_group: the normed group instance on the completion of a normed group

@[protected, instance]

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

has_norm (uniform_space.completion V)

Equations

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

@[simp]

theorem uniform_space.completion.norm_coe {V : Type u_1} [semi_normed_group V] (v : V) :

∥↑v∥ = ∥v∥

@[protected, instance]

def uniform_space.completion.normed_group (V : Type u_1) [semi_normed_group V] :

normed_group (uniform_space.completion V)

Equations

uniform_space.completion.normed_group V = {to_has_norm := uniform_space.completion.has_norm V semi_normed_group.to_has_norm, to_add_comm_group := {add := add_comm_group.add (show add_comm_group (uniform_space.completion V), from uniform_space.completion.add_comm_group), add_assoc := _, zero := add_comm_group.zero (show add_comm_group (uniform_space.completion V), from uniform_space.completion.add_comm_group), zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul (show add_comm_group (uniform_space.completion V), from uniform_space.completion.add_comm_group), nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg (show add_comm_group (uniform_space.completion V), from uniform_space.completion.add_comm_group), sub := add_comm_group.sub (show add_comm_group (uniform_space.completion V), from uniform_space.completion.add_comm_group), sub_eq_add_neg := _, gsmul := add_comm_group.gsmul (show add_comm_group (uniform_space.completion V), from uniform_space.completion.add_comm_group), gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _}, to_metric_space := {to_pseudo_metric_space := metric_space.to_pseudo_metric_space (show metric_space (uniform_space.completion V), from metric.completion.metric_space), eq_of_dist_eq_zero := _}, dist_eq := _}