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
.
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≤ c → a ≤ 1 → b * a ≤ c→ a ≤ 1 → b * a ≤ c≤ 1 → b * a ≤ c→ b * a ≤ c≤ 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≤ c → 1 ≤ a → b ≤ c * a→ 1 ≤ a → b ≤ c * a≤ a → b ≤ c * a→ b ≤ c * a≤ 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≤ 1 → b ≤ c → a * b ≤ c→ b ≤ c → a * b ≤ c≤ c → a * b ≤ c→ a * b ≤ c≤ 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≤ a → b ≤ c → b ≤ a * c→ b ≤ c → b ≤ a * c≤ c → b ≤ a * c→ b ≤ a * c≤ 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
.
Alias of Left.mul_lt_one_of_le_of_lt
.
Alias of Left.mul_lt_one_of_lt_of_le
.
Alias of Left.mul_lt_one
.
Alias of Left.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
.
Alias of Left.one_lt_mul_of_le_of_lt
.
Alias of Left.one_lt_mul_of_lt_of_le
.
Alias of Left.one_lt_mul
.
Alias of Left.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'
.
An additive semigroup with a partial order and satisfying AddLeftCancelSemigroup
(i.e. c + a < c + b → a < b→ a < b
) is a left_cancel AddSemigroup
.
A semigroup with a partial order and satisfying LeftCancelSemigroup
(i.e. a * c < b * c → a < b→ a < b
) is a left_cancel Semigroup
.
An additive semigroup with a partial order and satisfying AddRightCancelSemigroup
(a + c < b + c → a < b→ a < b
) is a right_cancel AddSemigroup
.
A semigroup with a partial order and satisfying RightCancelSemigroup
(i.e. a * c < b * c → a < b→ a < b
) is a right_cancel Semigroup
.
Alias of Left.mul_eq_mul_iff_eq_and_eq
.
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.
The sum of two strictly monotone functions is strictly monotone.
The product of two strictly monotone functions is strictly monotone.
The sum of two strictly monotone functions is strictly monotone.
The product of two strictly monotone functions is strictly monotone.