Theorems · Definition · order theory
AddLeftStrictMono
(M : Type u_1) → [Add M] → [LT M] → Prop
Typeclass for monotonicity of addition on the left,
namely b₁ < b₂ → a + b₁ < a + b₂.
You should usually not use this very granular typeclass directly, but rather a typeclass like
IsOrderedAddMonoid.
- Cited by
- 203 results in Mathlib
- Foundations
- Depth 4 from the axioms, rests on 10 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CovariantClassproof · cited by 25
Cited by204
Results whose statement or proof uses this declaration.
- lt_add_onestatement and proof · cited by 105
- neg_posstatement · cited by 74
- one_lt_twostatement and proof · cited by 67
- lt_add_of_pos_rightstatement and proof · cited by 51
- add_lt_add_rightstatement and proof · cited by 50
- neg_lt_neg_iffstatement and proof · cited by 39
- neg_lt_zerostatement · cited by 36
- add_lt_addstatement · cited by 35
- add_lt_add_of_le_of_ltstatement and proof · cited by 31
- sub_lt_iff_lt_add'statement and proof · cited by 30
- add_lt_add_iff_leftstatement and proof · cited by 30
- add_posstatement · cited by 28
Showing the 200 most cited of 204.