Theorems · Inductive type · functional analysis
NormedAddGroup
Type u_8 → Type u_8
A normed group is an additive 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
- 32 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 by51
Results whose statement or proof uses this declaration.
- norm_pos_iffstatement and proof · cited by 168
- norm_ne_zero_iffstatement and proof · cited by 65
- norm_eq_zerostatement and proof · cited by 43
- norm_le_zero_iffstatement and proof · cited by 23
- eq_zero_or_norm_posstatement and proof · cited by 6
- nnnorm_eq_zerostatement and proof · cited by 6
- nnnorm_ne_zero_iffstatement and proof · cited by 6
- norm_sub_eq_zero_iffstatement and proof · cited by 4
- HasCompactSupport.normstatement and proof · cited by 4
- Continuous.bounded_above_of_compact_supportstatement and proof · cited by 3
- ProbabilityTheory.IndepFun.integrable_left_of_integrable_opstatement and proof · cited by 3
- eq_zero_or_nnnorm_posstatement and proof · cited by 2