Theorems · Theorem · real analysis
ENNReal.toReal_pos
∀ {a : ENNReal}, a ≠ 0 → a ≠ ⊤ → 0 < a.toReal- Defined in
- Mathlib.Data.ENNReal.Real
- Cited by
- 59 results in Mathlib
- Foundations
- Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- ENNRealstatement and proof · cited by 9,879
- Top.topstatement and proof · cited by 9,680
- ENNReal.toRealstatement · cited by 859
- lt_top_iff_ne_topproof · cited by 95
- bot_lt_iff_ne_botproof · cited by 57
- ENNReal.toReal_pos_iffproof · cited by 20
Cited by59
Results whose statement or proof uses this declaration.
- ENNReal.trichotomyproof · cited by 29
- MeasureTheory.eLpNorm_zeroproof · cited by 14
- MeasureTheory.eLpNorm_measure_zeroproof · cited by 13
- MeasureTheory.MemLp.mono_exponentproof · cited by 11
- MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_topproof · cited by 9
- MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrictproof · cited by 8
- lp.norm_apply_le_normproof · cited by 6
- MeasureTheory.eLpNorm_constproof · cited by 5
- MeasureTheory.eLpNorm_eq_zero_iffproof · cited by 5
- MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_topproof · cited by 5
- MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mulproof · cited by 5
- MeasureTheory.meas_ge_le_mul_pow_eLpNorm_enormproof · cited by 4