Theorems · Theorem · real analysis
ENNReal.trichotomy
∀ (p : ENNReal), p = 0 ∨ p = ⊤ ∨ 0 < p.toReal
- Defined in
- Mathlib.Data.ENNReal.Real
- Cited by
- 29 results in Mathlib
- Foundations
- Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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 · cited by 9,680
- ENNReal.toRealstatement · cited by 859
- ENNReal.toReal_posproof · cited by 59
Cited by29
Results whose statement or proof uses this declaration.
- memℓp_genproof · cited by 8
- lp.norm_nonneg'proof · cited by 6
- ENNReal.log_mul_addproof · cited by 4
- ENNReal.log_rpowproof · cited by 4
- MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnormproof · cited by 4
- lp.norm_zeroproof · cited by 3
- Memℓp.const_smulproof · cited by 3
- MeasureTheory.eLpNorm_le_eLpNorm_top_mul_eLpNormproof · cited by 3
- memℓp_norm_iffproof · cited by 2
- Memℓp.addproof · cited by 2
- Memℓp.allproof · cited by 2
- ENNReal.trichotomy₂proof · cited by 2