Theorems · Inductive type · order theory
AddLeftReflectLE
(M : Type u_1) → [Add M] → [LE M] → Prop
Typeclass for 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
IsOrderedCancelAddMonoid.
- Cited by
- 119 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 3 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by123
Results whose statement or proof uses this declaration.
- add_tsub_cancel_rightstatement and proof · cited by 172
- Contravariant.AddLECancellablestatement and proof · cited by 45
- add_le_add_iff_leftstatement and proof · cited by 45
- add_tsub_cancel_leftstatement and proof · cited by 42
- tsub_add_eq_add_tsubstatement and proof · cited by 23
- add_tsub_assoc_of_lestatement and proof · cited by 16
- le_of_add_le_add_leftstatement and proof · cited by 15
- le_add_iff_nonneg_rightstatement and proof · cited by 15
- tsub_mulstatement and proof · cited by 14
- tsub_eq_iff_eq_add_of_lestatement and proof · cited by 12
- mul_tsubstatement and proof · cited by 11
- eq_tsub_of_add_eqstatement and proof · cited by 11