Theorems · Definition · order theory
AddRightStrictMono
(M : Type u_1) → [Add M] → [LT M] → Prop
Typeclass for monotonicity of addition on the right,
namely a₁ < a₂ → a₁ + b < a₂ + b.
You should usually not use this very granular typeclass directly, but rather a typeclass like
IsOrderedAddMonoid.
- Cited by
- 160 results in Mathlib
- Foundations
- Depth 4 from the axioms, rests on 11 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Function.swapproof · cited by 216
- CovariantClassproof · cited by 25
Cited by161
Results whose statement or proof uses this declaration.
- sub_posstatement and proof · cited by 147
- add_lt_add_leftstatement and proof · cited by 47
- add_lt_add_iff_rightstatement and proof · cited by 42
- sub_pos_of_ltstatement and proof · cited by 40
- mul_pos_of_neg_of_negstatement and proof · cited by 40
- neg_lt_neg_iffstatement and proof · cited by 39
- sub_lt_iff_lt_addstatement and proof · cited by 39
- add_lt_add_of_lt_of_lestatement and proof · cited by 37
- add_lt_addstatement · cited by 35
- lt_sub_iff_add_ltstatement and proof · cited by 24
- sub_negstatement and proof · cited by 22
- neg_ltstatement and proof · cited by 21