Theorems · Theorem · real analysis
ENNReal.coe_sub
∀ {r p : NNReal}, ↑(r - p) = ↑r - ↑pThis is a special case of WithTop.coe_sub in the ENNReal namespace
- Defined in
- Mathlib.Data.ENNReal.Operations
- Cited by
- 10 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.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement · cited by 9,879
- NNRealstatement and proof · cited by 4,310
- ENNReal.ofNNRealstatement · cited by 1,279
- WithTop.coe_subproof · cited by 1
Cited by10
Results whose statement or proof uses this declaration.
- ENNReal.tsum_geometricproof · cited by 8
- PMF.binomial_applyproof · cited by 4
- ENNReal.natCast_subproof · cited by 4
- NNReal.summable_schlomilch_iffproof · cited by 2
- MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image_aux1proof · cited by 1
- ENat.le_ceilproof · cited by 1
- PMF.support_bernoulliproof · cited by 1
- blimsup_cthickening_ae_le_of_eventually_mul_le_auxproof · cited by 1
- SpectrumRestricts.nnreal_iff_spectralRadius_leproof · cited by 1
- PMF.binomial_one_eq_bernoulliproof · cited by 0