Theorems · Definition · functional analysis
NNNorm.nnnorm
{E : Type u_8} → [self : NNNorm E] → E → NNRealthe ℝ≥0-valued norm function.
- Defined in
- Mathlib.Analysis.Normed.Group.Defs
- Cited by
- 952 results in Mathlib
- Foundations
- Depth 96 from the axioms, rests on 1,955 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- NNNorm
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by964
Results whose statement or proof uses this declaration.
- nnnorm_zerostatement · cited by 40
- spectralRadiusproof · cited by 36
- coe_nnnormstatement · cited by 33
- edist_zero_rightproof · cited by 25
- ContinuousLinearMap.lipschitzstatement and proof · cited by 16
- nnnorm_invstatement · cited by 14
- nnnorm_smulstatement · cited by 14
- nnnorm_negstatement · cited by 13
- Pi.nnnorm_defstatement and proof · cited by 12
- nndist_eq_nnnormstatement · cited by 11
- nnnorm_onestatement · cited by 11
- nnnorm_mulstatement · cited by 10
Showing the 200 most cited of 964.