Theorems · Theorem · real analysis
EReal.add_lt_add
∀ {x y z t : EReal}, x < y → z < t → x + z < y + t- Defined in
- Mathlib.Data.EReal.Operations
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realproof · cited by 25,697
- Bot.botproof · cited by 4,720
- le_reflproof · cited by 2,061
- le_of_ltproof · cited by 1,175
- eq_or_neproof · cited by 1,117
- LE.le.trans_ltproof · cited by 795
- ERealstatement and proof · cited by 793
- add_le_addproof · cited by 666
- bot_leproof · cited by 306
- Real.toERealproof · cited by 303
- LT.lt.ne_topproof · cited by 34
- EReal.bot_addproof · cited by 14
Cited by12
Results whose statement or proof uses this declaration.
- EReal.le_liminf_addproof · cited by 4
- EReal.limsup_add_leproof · cited by 4
- EReal.continuousAt_add_bot_coeproof · cited by 2
- EReal.le_limsup_addproof · cited by 2
- EReal.continuousAt_add_top_coeproof · cited by 2
- EReal.liminf_add_leproof · cited by 2
- EReal.add_lt_topproof · cited by 2
- EReal.continuousAt_add_bot_botproof · cited by 1
- EReal.continuousAt_add_top_topproof · cited by 1
- EReal.add_lt_add_of_lt_of_le'proof · cited by 1
- EReal.sub_lt_sub_of_le_of_gtproof · cited by 0
- EReal.liminf_add_gt_of_gtproof · cited by 0