Theorems · Theorem · real analysis
ENNReal.log_ofReal
∀ (x : ℝ), (ENNReal.ofReal x).log = if x ≤ 0 then ⊥ else ↑(Real.log x)
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 170 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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
- Top.topproof · cited by 9,680
- Bot.botstatement and proof · cited by 4,720
- LT.lt.leproof · cited by 2,189
- Real.logstatement and proof · cited by 939
- ENNReal.ofRealstatement and proof · cited by 863
- ENNReal.toRealproof · cited by 859
- ERealstatement · cited by 793
- not_leproof · cited by 328
- Real.toERealstatement and proof · cited by 303
- ENNReal.toReal_ofRealproof · cited by 82
- ENNReal.logstatement · cited by 72
Cited by3
Results whose statement or proof uses this declaration.
- EReal.log_expproof · cited by 6
- ENNReal.log_ofReal_of_posproof · cited by 1
- ENNReal.log_surjectiveproof · cited by 1