Theorems · Definition · functional analysis
AddGroupNorm.toNormedAddGroup
{E : Type u_5} → [inst : AddGroup E] → AddGroupNorm E → NormedAddGroup EConstruct 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
- 0 results in Mathlib
- Foundations
- Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddGroupstatement and proof · cited by 4,410
- SeminormedAddGroupproof · cited by 331
- NormedAddGroupstatement · cited by 32
- AddGroupNormstatement and proof · cited by 16
- SeminormedAddGroup.dist_eqproof · cited by 3
- AddGroupNorm.toAddGroupSeminormproof · cited by 2
- AddGroupSeminorm.toSeminormedAddGroupproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- AddGroupNorm.toNormedAddCommGroupproof · cited by 2