Theorems · Definition · order theory
AddRightMono
(M : Type u_1) → [Add M] → [LE 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
- 367 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 by371
Results whose statement or proof uses this declaration.
- add_le_addstatement and proof · cited by 666
- abs_nonnegstatement and proof · cited by 168
- sub_nonnegstatement and proof · cited by 167
- Right.add_pos_of_nonneg_of_posstatement and proof · cited by 137
- neg_le_neg_iffstatement and proof · cited by 57
- sub_le_iff_le_addstatement and proof · cited by 50
- add_le_add_iff_rightstatement and proof · cited by 47
- mul_nonneg_of_nonpos_of_nonposstatement and proof · cited by 45
- sub_le_sub_leftstatement and proof · cited by 43
- abs_ltstatement and proof · cited by 43
- le_sub_iff_add_lestatement and proof · cited by 41
- sub_nonneg_of_lestatement and proof · cited by 37
Showing the 200 most cited of 371.