Ordered monoids #
This file develops the basics of ordered monoids.
Implementation details #
Unfortunately, the number of '
appended to lemmas in this file
may differ between the multiplicative and the additive version of a lemma.
The reason is that we did not want to change existing names in the library.
Remark #
Almost no monoid is actually present in this file: most assumptions have been generalized to
Mul
or MulOneClass
.
Equations
Equations
Alias of add_lt_add_of_lt_of_lt
.
Only assumes left strict covariance
Only assumes left strict covariance.
Only assumes right strict covariance
Only assumes right strict covariance.
Lemmas of the form b ≤ c → a ≤ 1 → b * a ≤ c
,
which assume left covariance.
Assumes left covariance.
The lemma assuming right covariance is Right.add_nonpos
.
Assumes left covariance.
The lemma assuming right covariance is Right.mul_le_one
.
Assumes left covariance.
The lemma assuming right covariance is Right.add_neg_of_nonpos_of_neg
.
Assumes left covariance.
The lemma assuming right covariance is Right.mul_lt_one_of_le_of_lt
.
Assumes left covariance.
The lemma assuming right covariance is Right.add_neg_of_neg_of_nonpos
.
Assumes left covariance.
The lemma assuming right covariance is Right.mul_lt_one_of_lt_of_le
.
Assumes left covariance.
The lemma assuming right covariance is Right.add_neg
.
Assumes left covariance.
The lemma assuming right covariance is Right.mul_lt_one
.
Assumes left covariance.
The lemma assuming right covariance is Right.add_neg'
.
Assumes left covariance.
The lemma assuming right covariance is Right.mul_lt_one'
.
Lemmas of the form b ≤ c → 1 ≤ a → b ≤ c * a
,
which assume left covariance.
Assumes left covariance.
The lemma assuming right covariance is Right.add_nonneg
.
Assumes left covariance.
The lemma assuming right covariance is Right.one_le_mul
.
Assumes left covariance.
The lemma assuming right covariance is Right.add_pos_of_nonneg_of_pos
.
Assumes left covariance.
The lemma assuming right covariance is Right.one_lt_mul_of_le_of_lt
.
Assumes left covariance.
The lemma assuming right covariance is Right.add_pos_of_pos_of_nonneg
.
Assumes left covariance.
The lemma assuming right covariance is Right.one_lt_mul_of_lt_of_le
.
Assumes left covariance.
The lemma assuming right covariance is Right.add_pos
.
Assumes left covariance.
The lemma assuming right covariance is Right.one_lt_mul
.
Assumes left covariance.
The lemma assuming right covariance is Right.add_pos'
.
Assumes left covariance.
The lemma assuming right covariance is Right.one_lt_mul'
.
Lemmas of the form a ≤ 1 → b ≤ c → a * b ≤ c
,
which assume right covariance.
Assumes right covariance.
The lemma assuming left covariance is Left.add_nonpos
.
Assumes right covariance.
The lemma assuming left covariance is Left.mul_le_one
.
Assumes right covariance.
The lemma assuming left covariance is Left.add_neg_of_neg_of_nonpos
.
Assumes right covariance.
The lemma assuming left covariance is Left.mul_lt_one_of_lt_of_le
.
Assumes right covariance.
The lemma assuming left covariance is Left.add_neg_of_nonpos_of_neg
.
Assumes right covariance.
The lemma assuming left covariance is Left.mul_lt_one_of_le_of_lt
.
Assumes right covariance.
The lemma assuming left covariance is Left.add_neg
.
Assumes right covariance.
The lemma assuming left covariance is Left.mul_lt_one
.
Assumes right covariance.
The lemma assuming left covariance is Left.add_neg'
.
Assumes right covariance.
The lemma assuming left covariance is Left.mul_lt_one'
.
Lemmas of the form 1 ≤ a → b ≤ c → b ≤ a * c
,
which assume right covariance.
Assumes right covariance.
The lemma assuming left covariance is Left.add_nonneg
.
Assumes right covariance.
The lemma assuming left covariance is Left.one_le_mul
.
Assumes right covariance.
The lemma assuming left covariance is Left.add_pos_of_pos_of_nonneg
.
Assumes right covariance.
The lemma assuming left covariance is Left.one_lt_mul_of_lt_of_le
.
Assumes right covariance.
The lemma assuming left covariance is Left.add_pos_of_nonneg_of_pos
.
Assumes right covariance.
The lemma assuming left covariance is Left.one_lt_mul_of_le_of_lt
.
Assumes right covariance.
The lemma assuming left covariance is Left.add_pos
.
Assumes right covariance.
The lemma assuming left covariance is Left.one_lt_mul
.
Assumes right covariance.
The lemma assuming left covariance is Left.add_pos'
.
Assumes right covariance.
The lemma assuming left covariance is Left.one_lt_mul'
.
Alias of Left.mul_le_one
.
Assumes left covariance.
The lemma assuming right covariance is Right.mul_le_one
.
Alias of Left.mul_lt_one_of_le_of_lt
.
Assumes left covariance.
The lemma assuming right covariance is Right.mul_lt_one_of_le_of_lt
.
Alias of Left.mul_lt_one_of_lt_of_le
.
Assumes left covariance.
The lemma assuming right covariance is Right.mul_lt_one_of_lt_of_le
.
Alias of Left.mul_lt_one
.
Assumes left covariance.
The lemma assuming right covariance is Right.mul_lt_one
.
Alias of Left.mul_lt_one'
.
Assumes left covariance.
The lemma assuming right covariance is Right.mul_lt_one'
.
Alias of Left.add_nonpos
.
Alias of Left.add_neg_of_nonpos_of_neg
.
Alias of Left.add_neg_of_neg_of_nonpos
.
Alias of Left.add_neg
.
Alias of Left.add_neg'
.
Alias of Left.one_le_mul
.
Assumes left covariance.
The lemma assuming right covariance is Right.one_le_mul
.
Alias of Left.one_lt_mul_of_le_of_lt
.
Assumes left covariance.
The lemma assuming right covariance is Right.one_lt_mul_of_le_of_lt
.
Alias of Left.one_lt_mul_of_lt_of_le
.
Assumes left covariance.
The lemma assuming right covariance is Right.one_lt_mul_of_lt_of_le
.
Alias of Left.one_lt_mul
.
Assumes left covariance.
The lemma assuming right covariance is Right.one_lt_mul
.
Alias of Left.one_lt_mul'
.
Assumes left covariance.
The lemma assuming right covariance is Right.one_lt_mul'
.
Alias of Left.add_nonneg
.
Alias of Left.add_pos_of_nonneg_of_pos
.
Alias of Left.add_pos_of_pos_of_nonneg
.
Alias of Left.add_pos
.
Alias of Left.add_pos'
.
Alias of mul_eq_one_iff_of_one_le
.
Alias of add_eq_zero_iff_of_nonneg
.
An additive semigroup with a partial order and satisfying AddLeftCancelSemigroup
(i.e. c + a < c + b → a < b
) is a left_cancel AddSemigroup
.
Equations
- Contravariant.toAddLeftCancelSemigroup = AddLeftCancelSemigroup.mk ⋯
Instances For
A semigroup with a partial order and satisfying LeftCancelSemigroup
(i.e. a * c < b * c → a < b
) is a left_cancel Semigroup
.
Equations
- Contravariant.toLeftCancelSemigroup = LeftCancelSemigroup.mk ⋯
Instances For
An additive semigroup with a partial order and satisfying AddRightCancelSemigroup
(a + c < b + c → a < b
) is a right_cancel AddSemigroup
.
Equations
- Contravariant.toAddRightCancelSemigroup = AddRightCancelSemigroup.mk ⋯
Instances For
A semigroup with a partial order and satisfying RightCancelSemigroup
(i.e. a * c < b * c → a < b
) is a right_cancel Semigroup
.
Equations
- Contravariant.toRightCancelSemigroup = RightCancelSemigroup.mk ⋯
Instances For
The sum of two monotone functions is monotone.
The product of two monotone functions is monotone.
The sum of two monotone functions is monotone.
The product of two monotone functions is monotone.
The sum of two antitone functions is antitone.
The product of two antitone functions is antitone.
The sum of two antitone functions is antitone.
The product of two antitone functions is antitone.