Theorems · Definition · functional analysis
ENorm.enorm
{E : Type u_8} → [self : ENorm E] → E → ENNRealthe ℝ≥0∞-valued norm function.
- Defined in
- Mathlib.Analysis.Normed.Group.Defs
- Cited by
- 715 results in Mathlib
- Foundations
- Depth 97 from the axioms, rests on 1,957 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- ENorm
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 by762
Results whose statement or proof uses this declaration.
- MeasureTheory.VectorMeasure.variationproof · cited by 125
- MeasureTheory.HasFiniteIntegralproof · cited by 120
- enorm_ne_topstatement · cited by 82
- egaugeproof · cited by 75
- MeasureTheory.eLpNorm'proof · cited by 73
- MeasureTheory.memLp_one_iff_integrableproof · cited by 73
- MeasureTheory.eLpNormEssSupproof · cited by 59
- enorm_zerostatement · cited by 44
- ofReal_normstatement · cited by 39
- edist_eq_enorm_substatement and proof · cited by 37
- MeasureTheory.integrable_indicator_iffproof · cited by 30
- MeasureTheory.AEStronglyMeasurable.enormstatement · cited by 29
Showing the 200 most cited of 762.