Structures · Algebra
AddLeftReflectLE
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.
- Shape
- One type argument · adds le_of_add_le_add_left
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances7
- Finsupp
- DFinsupp
- PNat
- Ordinal
- Subtype
- OrderDual
- Multiset
How is a type an instance?
Loading the hierarchy index…
Assumed by128
- add_tsub_cancel_right
- add_le_add_iff_left
- Contravariant.AddLECancellable
- add_tsub_cancel_left
- tsub_add_eq_add_tsub
- add_tsub_assoc_of_le
- le_add_iff_nonneg_right
- le_of_add_le_add_left
- tsub_mul
- tsub_eq_iff_eq_add_of_le
- mul_tsub
- le_tsub_of_add_le_left
- eq_tsub_of_add_eq
- tsub_tsub_cancel_of_le
- add_le_iff_nonpos_right
- tsub_eq_of_eq_add
- tsub_lt_self
- le_tsub_of_add_le_right
- eq_tsub_iff_add_eq_of_le
- mul_nonneg_iff
- le_tsub_iff_right
- le_tsub_iff_left
- add_tsub_add_eq_tsub_right
- exists_nonneg_add_of_le
- WithTop.addLECancellable_of_ne_top
- Nat.cast_tsub
- mul_add_mul_le_mul_add_mul
- tsub_lt_tsub_iff_left_of_le
- two_mul_le_add_sq
- add_tsub_add_eq_tsub_left
- tsub_tsub_assoc
- tsub_lt_iff_right
- WithTop.le_of_add_le_add_left
- mul_nonneg_iff_pos_imp_nonneg
- four_mul_le_sq_add
- WithBot.le_of_add_le_add_left
- WithBot.addLECancellable_of_ne_bot
- geom_sum₂_mul_of_ge
- nonneg_of_le_add_right
- tsub_add_tsub_comm
- AddLeftReflectLE.le_of_add_le_add_left
- mul_nonpos_iff
- WithTop.add_le_add_iff_left
- mul_self_tsub_mul_self
- tsub_le_tsub_iff_left
- geom_sum₂_mul_of_le
- Finset.HasAntidiagonal.filter_fst_eq_antidiagonal
- Finset.sup'_add'
- Finset.add_sup
- two_mul_le_add_of_sq_le_mul
Ancestors0
No ancestors.