Theorems · Definition · order theory
AddLeftReflectLT
(M : Type u_1) → [Add M] → [LT M] → Prop
Typeclass for strict reverse monotonicity of addition on the left,
namely a + b₁ < a + b₂ → b₁ < b₂.
You should usually not use this very granular typeclass directly, but rather a typeclass like
IsOrderedAddMonoid.
- Cited by
- 33 results in Mathlib
- Foundations
- Depth 4 from the axioms · 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.
- ContravariantClassproof · cited by 15
Cited by33
Results whose statement or proof uses this declaration.
- add_lt_add_iff_leftstatement and proof · cited by 30
- mul_self_posstatement and proof · cited by 17
- le_of_forall_pos_le_addstatement and proof · cited by 15
- lt_add_iff_pos_rightstatement and proof · cited by 13
- lt_of_add_lt_add_leftstatement and proof · cited by 9
- mul_pos_iffstatement and proof · cited by 8
- exists_pos_add_of_lt'statement and proof · cited by 5
- pos_of_lt_add_rightstatement and proof · cited by 4
- le_iff_forall_pos_le_addstatement and proof · cited by 4
- WithBot.add_lt_add_iff_leftstatement and proof · cited by 3
- add_lt_iff_neg_leftstatement and proof · cited by 2
- AddLECancellable.lt_of_tsub_lt_tsub_left_of_lestatement and proof · cited by 2