Theorems · Theorem · real analysis
ENNReal.le_of_forall_pos_le_add
∀ {a b : ENNReal}, (∀ (ε : NNReal), 0 < ε → b < ⊤ → a ≤ b + ↑ε) → a ≤ b- Defined in
- Mathlib.Data.ENNReal.Basic
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 128 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement and proof · cited by 9,879
- Top.topstatement and proof · cited by 9,680
- NNRealstatement and proof · cited by 4,310
- ENNReal.ofNNRealstatement and proof · cited by 1,279
- LT.lt.trans_leproof · cited by 678
- le_topproof · cited by 411
- ENNReal.lt_iff_exists_add_pos_ltproof · cited by 3
Cited by15
Results whose statement or proof uses this declaration.
- Metric.infEDist_closureproof · cited by 8
- VitaliFamily.measure_le_of_frequently_leproof · cited by 5
- Metric.infEDist_le_infEDist_add_hausdorffEDistproof · cited by 4
- MeasureTheory.Content.measure_eq_content_of_regularproof · cited by 3
- Metric.cthickening_eq_iInter_cthickening'proof · cited by 3
- Metric.ediam_cthickening_leproof · cited by 2
- StieltjesFunction.outer_Iocproof · cited by 2
- MeasureTheory.levyProkhorovEDist_le_of_forall_add_pos_leproof · cited by 2
- RealRMK.measure_le_of_isCompact_of_integralproof · cited by 1
- MeasureTheory.preVariation.sum_le_preVariationFun_iUnionproof · cited by 1
- MeasureTheory.FiniteMeasure.limsup_measure_closed_le_of_tendstoproof · cited by 1
- MeasureTheory.limsup_measure_closed_le_of_forall_tendsto_measureproof · cited by 1