Theorems · Theorem · real analysis
ENNReal.coe_add
∀ (x y : NNReal), ↑(x + y) = ↑x + ↑y
- Defined in
- Mathlib.Data.ENNReal.Basic
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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
Cited by12
Results whose statement or proof uses this declaration.
- ENNReal.ofReal_addproof · cited by 26
- ENNReal.ofNNRealHomproof · cited by 6
- ENNReal.lt_iff_exists_add_pos_ltproof · cited by 3
- MeasureTheory.exists_pos_setLIntegral_lt_of_measure_ltproof · cited by 1
- MeasureTheory.exists_simpleFunc_forall_lintegral_sub_lt_of_posproof · cited by 1
- Disjoint.exists_thickeningsproof · cited by 1
- tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_supportproof · cited by 1
- ENNReal.young_inequalityproof · cited by 1
- Real.volume_closedEBallproof · cited by 1
- Real.volume_eballproof · cited by 1
- eHolderNorm_add_leproof · cited by 0
- ENNReal.young_inequality_eq_iffproof · cited by 0