Theorems · Theorem · real analysis
ENNReal.ofReal_eq_zero
∀ {p : ℝ}, ENNReal.ofReal p = 0 ↔ p ≤ 0- Defined in
- Mathlib.Data.ENNReal.Real
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- ENNRealstatement · cited by 9,879
- ENNReal.ofRealstatement · cited by 863
Cited by11
Results whose statement or proof uses this declaration.
- ENNReal.ofReal_of_nonposproof · cited by 9
- Metric.cthickening_of_nonposproof · cited by 8
- ENNReal.zero_eq_ofRealproof · cited by 3
- AddCircle.closedBall_ae_eq_ballproof · cited by 2
- MeasureTheory.eLpNorm_enorm_rpowproof · cited by 2
- MeasureTheory.withDensity_ofReal_mutuallySingularproof · cited by 1
- NumberField.mixedEmbedding.convexBodySum_volumeproof · cited by 1
- MeasureTheory.integral_mul_norm_le_Lp_mul_Lqproof · cited by 1
- StieltjesFunction.length_subadditive_Icc_Iooproof · cited by 1
- ProbabilityTheory.lintegral_exponentialPDF_eq_antiDerivproof · cited by 1
- Real.Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gammaproof · cited by 1