Theorems · Inductive type · functional analysis
ENorm
Type u_8 → Type u_8
Auxiliary class, endowing a type α with a function enorm : α → ℝ≥0∞ with notation ‖x‖ₑ.
- Defined in
- Mathlib.Analysis.Normed.Group.Defs
- Cited by
- 155 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 by185
Results whose statement or proof uses this declaration.
- ENorm.enormstatement and proof · cited by 715
- MeasureTheory.MemLpstatement and proof · cited by 457
- MeasureTheory.eLpNormstatement and proof · cited by 329
- MeasureTheory.HasFiniteIntegralstatement and proof · cited by 120
- egaugestatement and proof · cited by 75
- MeasureTheory.eLpNorm'statement and proof · cited by 73
- Asymptotics.IsLittleOTVSstatement · cited by 73
- Asymptotics.IsBigOTVSstatement · cited by 61
- MeasureTheory.eLpNormEssSupstatement and proof · cited by 59
- MeasureTheory.eLpNorm_congr_aestatement and proof · cited by 48
- MeasureTheory.eLpNorm_exponent_zerostatement and proof · cited by 43
- MeasureTheory.eLpNorm_exponent_topstatement and proof · cited by 36