Theorems · Theorem · order theory
WithTop.add_lt_add
∀ {α : Type u} [inst : Add α] {w x y z : WithTop α} [inst_1 : Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α],
x < z → y < w → x + y < z + w- Cited by
- 2 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Top.topproof · cited by 9,680
- Preorderstatement and proof · cited by 7,952
- WithTopstatement and proof · cited by 3,754
- LT.lt.leproof · cited by 2,189
- WithTop.someproof · cited by 1,128
- LT.lt.trans_leproof · cited by 678
- AddLeftStrictMonostatement and proof · cited by 203
- AddRightStrictMonostatement and proof · cited by 160
- WithTop.recTopCoeproof · cited by 107
- WithTop.coe_ne_topproof · cited by 43
- LT.lt.ne_topproof · cited by 34
- WithTop.add_topproof · cited by 18
Cited by2
Results whose statement or proof uses this declaration.
- ENNReal.add_lt_addproof · cited by 13
- ENat.add_lt_addproof · cited by 1