Theorems · Theorem · real analysis
ENNReal.add_lt_add
∀ {a b c d : ENNReal}, a < c → b < d → a + b < c + d- Defined in
- Mathlib.Data.ENNReal.Operations
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 113 from the axioms · 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.
- ENNRealstatement and proof · cited by 9,879
- WithTop.add_lt_addproof · cited by 2
Cited by13
Results whose statement or proof uses this declaration.
- Metric.thickening_thickening_subsetproof · cited by 4
- IsCompact.uniform_oscillationWithinproof · cited by 2
- MeasureTheory.exists_measure_symmDiff_lt_of_generateFrom_isSetRingproof · cited by 2
- MeasurableSet.exists_isOpen_symmDiff_ltproof · cited by 1
- ENNReal.sum_lt_sum_of_nonemptyproof · cited by 1
- MeasureTheory.SimpleFunc.exists_lt_lintegral_simpleFunc_of_lt_lintegralproof · cited by 1
- VitaliFamily.ae_tendsto_lintegral_enorm_sub_div'_of_integrableproof · cited by 1
- MeasureTheory.Measure.tendsto_addHaar_inter_smul_zero_of_density_zeroproof · cited by 1
- Metric.eball_disjointproof · cited by 1
- edist_ne_top_of_mem_ballproof · cited by 0