Theorems · Theorem · real analysis
ENNReal.coe_toReal
∀ (r : NNReal), (↑r).toReal = ↑r
- Defined in
- Mathlib.Data.ENNReal.Basic
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 106 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
- NNRealstatement and proof · cited by 4,310
- ENNReal.ofNNRealstatement · cited by 1,279
- NNReal.toRealstatement · cited by 1,260
- ENNReal.toRealstatement · cited by 859
Cited by14
Results whose statement or proof uses this declaration.
- PiLp.nnnorm_singleproof · cited by 4
- ENNReal.toReal_smulproof · cited by 3
- MeasureTheory.Submartingale.upcrossings_ae_lt_top'proof · cited by 1
- BoxIntegral.HasIntegral.of_aeEq_zeroproof · cited by 1
- MeasureTheory.MemLp.eLpNormEssSup_indicator_norm_ge_eq_zeroproof · cited by 1
- ENNReal.ofReal_lt_coe_iffproof · cited by 1
- NumberField.mixedEmbedding.covolume_idealLatticeproof · cited by 1
- NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTopproof · cited by 1
- ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_forall_memLp_exp_mulproof · cited by 1
- RealRMK.measure_le_of_isCompact_of_integralproof · cited by 1
- tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_supportproof · cited by 1
- MeasureTheory.exists_lt_lowerSemicontinuous_integral_gt_nnrealproof · cited by 1