Theorems · Inductive type · functional analysis
NormedCommGroup
Type u_8 → Type u_8
A normed group is a group endowed with a norm for which dist x y = ‖x⁻¹ * y‖ defines a metric
space structure.
- Defined in
- Mathlib.Analysis.Normed.Group.Defs
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by21
Results whose statement or proof uses this declaration.
- IsUpperSet.thickening'statement and proof · cited by 1
- GroupNormClass.toNormedCommGroupstatement · cited by 1
- IsLowerSet.thickening'statement and proof · cited by 1
- NormedCommGroup.recOnstatement and proof · cited by 0
- Equiv.normedCommGroupstatement and proof · cited by 0
- lowerClosure_interior_subset'statement and proof · cited by 0
- GroupNorm.toNormedCommGroupstatement · cited by 0
- NormedCommGroup.mk.noConfusionstatement · cited by 0
- tendsto_norm_div_self_nhdsNEstatement and proof · cited by 0
- IsUpperSet.cthickening'statement and proof · cited by 0
- upperClosure_interior_subset'statement and proof · cited by 0
- IsLowerSet.cthickening'statement and proof · cited by 0