Theorems · Definition · real analysis
NNReal.toReal
NNReal → ℝ
Coercion ℝ≥0 → ℝ.
- Defined in
- Mathlib.Data.NNReal.Defs
- Cited by
- 1,260 results in Mathlib
- Foundations
- Depth 96 from the axioms, rests on 1,954 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by1,311
Results whose statement or proof uses this declaration.
- ENNReal.toRealproof · cited by 859
- Real.sqrtproof · cited by 545
- NNReal.eqstatement · cited by 201
- FormalMultilinearSeries.radiusproof · cited by 150
- NNReal.coe_nonnegstatement · cited by 130
- NNReal.coe_le_coestatement · cited by 73
- dimHproof · cited by 65
- ENNReal.ofReal_coe_nnrealstatement · cited by 52
- HolderWithproof · cited by 47
- HolderOnWithproof · cited by 44
- NNReal.rpow_oneproof · cited by 38
- ApproximatesLinearOnproof · cited by 38
Showing the 200 most cited of 1,311.