Theorems · Theorem · real analysis
ENNReal.le_ofReal_iff_toReal_le
∀ {a : ENNReal} {b : ℝ}, a ≠ ⊤ → 0 ≤ b → (a ≤ ENNReal.ofReal b ↔ a.toReal ≤ b)- Defined in
- Mathlib.Data.ENNReal.Real
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 110 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- ENNRealstatement and proof · cited by 9,879
- Top.topstatement and proof · cited by 9,680
- NNRealproof · cited by 4,310
- ENNReal.ofNNRealproof · cited by 1,279
- NNReal.toRealproof · cited by 1,260
- ENNReal.ofRealstatement · cited by 863
- ENNReal.toRealstatement · cited by 859
- Real.le_toNNReal_iff_coe_leproof · cited by 5
Cited by11
Results whose statement or proof uses this declaration.
- ENNReal.toReal_le_of_le_ofRealproof · cited by 14
- MeasureTheory.tendstoInMeasure_iff_distproof · cited by 1
- Metric.hausdorffDist_le_of_infDistproof · cited by 1
- MeasureTheory.smul_le_stoppedValue_hittingBtwnproof · cited by 1
- ProbabilityTheory.Kernel.HasSubgaussianMGF.measure_univ_le_oneproof · cited by 1
- ENNReal.toReal_limsupproof · cited by 1
- MeasureTheory.Lp.dense_hasCompactSupport_contDiffproof · cited by 0
- ProbabilityTheory.Kernel.isSFiniteKernel_withDensity_of_isFiniteKernelproof · cited by 0
- ProbabilityTheory.measure_limsup_eq_oneproof · cited by 0
- UniformFun.dist_leproof · cited by 0
- ENNReal.ofReal_iInfproof · cited by 0