Theorems · Definition · real analysis
ENNReal
Type
The extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.
- Defined in
- Mathlib.Data.ENNReal.Basic
- Cited by
- 9,879 results in Mathlib
- Foundations
- Depth 96 from the axioms, rests on 1,955 definitions · uses propext, Classical.choice, Quot.sound
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 by10,471
Results whose statement or proof uses this declaration.
- MeasureTheory.aestatement and proof · cited by 2,352
- ENNReal.ofNNRealstatement · cited by 1,279
- MeasureTheory.lintegralstatement · cited by 1,152
- ENNReal.ofRealstatement · cited by 863
- ENNReal.toRealstatement and proof · cited by 859
- EDist.ediststatement · cited by 735
- ENorm.enormstatement · cited by 715
- MeasureTheory.Lpstatement and proof · cited by 715
- MeasureTheory.MemLpstatement and proof · cited by 457
- WithLpstatement · cited by 345
- MeasureTheory.measure_monostatement and proof · cited by 338
- MeasureTheory.eLpNormstatement and proof · cited by 329
Showing the 200 most cited of 10,471.