Theorems · Theorem · real analysis
ENNReal.inv_zero
0⁻¹ = ⊤
- Defined in
- Mathlib.Data.ENNReal.Inv
- Cited by
- 37 results in Mathlib
- Foundations
- Depth 127 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement and proof · cited by 9,879
- Top.topstatement and proof · cited by 9,680
- Set.ofPredproof · cited by 6,101
- MulZeroClass.zero_mulproof · cited by 1,625
- InfSet.sInfproof · cited by 935
- sInf_emptyproof · cited by 12
Cited by37
Results whose statement or proof uses this declaration.
- ENNReal.inv_powproof · cited by 9
- ENNReal.tsum_geometricproof · cited by 8
- ENNReal.rpow_negproof · cited by 6
- ENNReal.div_zeroproof · cited by 5
- ENNReal.inv_strictAntiproof · cited by 4
- MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnormproof · cited by 4
- MeasureTheory.laverage_zero_measureproof · cited by 4
- ENNReal.zpow_negproof · cited by 3
- ENNReal.inv_rpowproof · cited by 3
- MeasureTheory.pdf.IsUniform.pdf_eqproof · cited by 3
- ENNReal.toNNReal_invproof · cited by 3
- MeasureTheory.eLpNorm_smul_measure_of_ne_zeroproof · cited by 3