Theorems · Definition · functional analysis

AddGroupNorm.toNormedAddCommGroup

{E : Type u_5} → [inst : AddCommGroup E] → AddGroupNorm E → NormedAddCommGroup E

Construct a normed group from a norm, i.e., registering the distance and the metric space structure from the norm properties. Note that in most cases this instance creates bad definitional equalities (e.g., it does not take into account a possibly existing UniformSpace instance on E).

Defined in

Mathlib.Analysis.Normed.Group.Defs

Cited by

2 results in Mathlib

Foundations

Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroup