Theorems · Theorem · real analysis
ENNReal.sub_mul
∀ {a b c : ENNReal}, (0 < b → b < a → c ≠ ⊤) → (a - b) * c = a * c - b * c- Defined in
- Mathlib.Data.ENNReal.Operations
- Cited by
- 8 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.
Cites12
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
- MulZeroClass.zero_mulproof · cited by 1,625
- le_or_gtproof · cited by 269
- tsub_zeroproof · cited by 123
- eq_zero_or_posproof · cited by 54
- ENNReal.mul_ne_topproof · cited by 41
- LT.lt.ne_topproof · cited by 34
- tsub_eq_zero_of_leproof · cited by 26
- ENNReal.cancel_of_neproof · cited by 23
- mul_left_monoproof · cited by 10
- AddLECancellable.tsub_mulproof · cited by 2
Cited by8
Results whose statement or proof uses this declaration.
- ENNReal.mul_subproof · cited by 3
- ENNReal.sub_divproof · cited by 2
- ContractingWith.edist_inequalityproof · cited by 1
- MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image_aux1proof · cited by 1
- MeasureTheory.Measure.tendsto_addHaar_inter_smul_one_of_density_one_auxproof · cited by 1
- blimsup_cthickening_ae_le_of_eventually_mul_le_auxproof · cited by 1
- lipschitzWith_thickenedIndicatorproof · cited by 1
- ENNReal.HolderConjugate.sub_one_mul_invproof · cited by 0