Theorems · Inductive type · functional analysis
Norm
Type u_8 → Type u_8
Auxiliary class, endowing a type E with a function norm : E → ℝ with notation ‖x‖. This
class is designed to be extended in more interesting classes specifying the properties of the norm.
- Defined in
- Mathlib.Analysis.Normed.Group.Defs
- Cited by
- 512 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · 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 by655
Results whose statement or proof uses this declaration.
- Norm.normstatement and proof · cited by 5,413
- Asymptotics.IsBigOstatement · cited by 506
- Asymptotics.IsLittleOstatement · cited by 375
- RingHomIsometricstatement · cited by 282
- norm_smulstatement and proof · cited by 242
- Asymptotics.IsBigOWithstatement · cited by 187
- norm_mulstatement and proof · cited by 171
- NormOneClass.norm_onestatement and proof · cited by 148
- NormOneClassstatement · cited by 136
- Asymptotics.IsThetastatement and proof · cited by 115
- NormSMulClassstatement · cited by 107
- NormMulClassstatement · cited by 66
Showing the 200 most cited of 655.