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
has_mul or mul_one_class.
theorem
mul_le_mul_left'
{α : Type u_1}
[has_mul α]
[has_le α]
[covariant_class α α has_mul.mul has_le.le]
{b c : α}
(bc : b ≤ c)
(a : α) :
theorem
add_le_add_left
{α : Type u_1}
[has_add α]
[has_le α]
[covariant_class α α has_add.add has_le.le]
{b c : α}
(bc : b ≤ c)
(a : α) :
theorem
le_of_mul_le_mul_left'
{α : Type u_1}
[has_mul α]
[has_le α]
[contravariant_class α α has_mul.mul has_le.le]
{a b c : α}
(bc : a * b ≤ a * c) :
b ≤ c
theorem
le_of_add_le_add_left
{α : Type u_1}
[has_add α]
[has_le α]
[contravariant_class α α has_add.add has_le.le]
{a b c : α}
(bc : a + b ≤ a + c) :
b ≤ c
theorem
add_le_add_right
{α : Type u_1}
[has_add α]
[has_le α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{b c : α}
(bc : b ≤ c)
(a : α) :
theorem
mul_le_mul_right'
{α : Type u_1}
[has_mul α]
[has_le α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{b c : α}
(bc : b ≤ c)
(a : α) :
theorem
le_of_mul_le_mul_right'
{α : Type u_1}
[has_mul α]
[has_le α]
[contravariant_class α α (function.swap has_mul.mul) has_le.le]
{a b c : α}
(bc : b * a ≤ c * a) :
b ≤ c
theorem
le_of_add_le_add_right
{α : Type u_1}
[has_add α]
[has_le α]
[contravariant_class α α (function.swap has_add.add) has_le.le]
{a b c : α}
(bc : b + a ≤ c + a) :
b ≤ c
@[simp]
theorem
mul_le_mul_iff_left
{α : Type u_1}
[has_mul α]
[has_le α]
[covariant_class α α has_mul.mul has_le.le]
[contravariant_class α α has_mul.mul has_le.le]
(a : α)
{b c : α} :
@[simp]
theorem
add_le_add_iff_left
{α : Type u_1}
[has_add α]
[has_le α]
[covariant_class α α has_add.add has_le.le]
[contravariant_class α α has_add.add has_le.le]
(a : α)
{b c : α} :
@[simp]
theorem
mul_le_mul_iff_right
{α : Type u_1}
[has_mul α]
[has_le α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
[contravariant_class α α (function.swap has_mul.mul) has_le.le]
(a : α)
{b c : α} :
@[simp]
theorem
add_le_add_iff_right
{α : Type u_1}
[has_add α]
[has_le α]
[covariant_class α α (function.swap has_add.add) has_le.le]
[contravariant_class α α (function.swap has_add.add) has_le.le]
(a : α)
{b c : α} :
@[simp]
theorem
mul_lt_mul_iff_left
{α : Type u_1}
[has_mul α]
[has_lt α]
[covariant_class α α has_mul.mul has_lt.lt]
[contravariant_class α α has_mul.mul has_lt.lt]
(a : α)
{b c : α} :
@[simp]
theorem
add_lt_add_iff_left
{α : Type u_1}
[has_add α]
[has_lt α]
[covariant_class α α has_add.add has_lt.lt]
[contravariant_class α α has_add.add has_lt.lt]
(a : α)
{b c : α} :
@[simp]
theorem
mul_lt_mul_iff_right
{α : Type u_1}
[has_mul α]
[has_lt α]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
[contravariant_class α α (function.swap has_mul.mul) has_lt.lt]
(a : α)
{b c : α} :
@[simp]
theorem
add_lt_add_iff_right
{α : Type u_1}
[has_add α]
[has_lt α]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
[contravariant_class α α (function.swap has_add.add) has_lt.lt]
(a : α)
{b c : α} :
theorem
add_lt_add_left
{α : Type u_1}
[has_add α]
[has_lt α]
[covariant_class α α has_add.add has_lt.lt]
{b c : α}
(bc : b < c)
(a : α) :
theorem
mul_lt_mul_left'
{α : Type u_1}
[has_mul α]
[has_lt α]
[covariant_class α α has_mul.mul has_lt.lt]
{b c : α}
(bc : b < c)
(a : α) :
theorem
lt_of_add_lt_add_left
{α : Type u_1}
[has_add α]
[has_lt α]
[contravariant_class α α has_add.add has_lt.lt]
{a b c : α}
(bc : a + b < a + c) :
b < c
theorem
lt_of_mul_lt_mul_left'
{α : Type u_1}
[has_mul α]
[has_lt α]
[contravariant_class α α has_mul.mul has_lt.lt]
{a b c : α}
(bc : a * b < a * c) :
b < c
theorem
mul_lt_mul_right'
{α : Type u_1}
[has_mul α]
[has_lt α]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
{b c : α}
(bc : b < c)
(a : α) :
theorem
add_lt_add_right
{α : Type u_1}
[has_add α]
[has_lt α]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
{b c : α}
(bc : b < c)
(a : α) :
theorem
lt_of_add_lt_add_right
{α : Type u_1}
[has_add α]
[has_lt α]
[contravariant_class α α (function.swap has_add.add) has_lt.lt]
{a b c : α}
(bc : b + a < c + a) :
b < c
theorem
lt_of_mul_lt_mul_right'
{α : Type u_1}
[has_mul α]
[has_lt α]
[contravariant_class α α (function.swap has_mul.mul) has_lt.lt]
{a b c : α}
(bc : b * a < c * a) :
b < c
@[simp]
theorem
le_add_iff_nonneg_right
{α : Type u_1}
[add_zero_class α]
[has_le α]
[covariant_class α α has_add.add has_le.le]
[contravariant_class α α has_add.add has_le.le]
(a : α)
{b : α} :
@[simp]
theorem
le_mul_iff_one_le_right'
{α : Type u_1}
[mul_one_class α]
[has_le α]
[covariant_class α α has_mul.mul has_le.le]
[contravariant_class α α has_mul.mul has_le.le]
(a : α)
{b : α} :
@[simp]
theorem
add_le_iff_nonpos_right
{α : Type u_1}
[add_zero_class α]
[has_le α]
[covariant_class α α has_add.add has_le.le]
[contravariant_class α α has_add.add has_le.le]
(a : α)
{b : α} :
@[simp]
theorem
mul_le_iff_le_one_right'
{α : Type u_1}
[mul_one_class α]
[has_le α]
[covariant_class α α has_mul.mul has_le.le]
[contravariant_class α α has_mul.mul has_le.le]
(a : α)
{b : α} :
@[simp]
theorem
le_add_iff_nonneg_left
{α : Type u_1}
[add_zero_class α]
[has_le α]
[covariant_class α α (function.swap has_add.add) has_le.le]
[contravariant_class α α (function.swap has_add.add) has_le.le]
(a : α)
{b : α} :
@[simp]
theorem
le_mul_iff_one_le_left'
{α : Type u_1}
[mul_one_class α]
[has_le α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
[contravariant_class α α (function.swap has_mul.mul) has_le.le]
(a : α)
{b : α} :
@[simp]
theorem
add_le_iff_nonpos_left
{α : Type u_1}
[add_zero_class α]
[has_le α]
[covariant_class α α (function.swap has_add.add) has_le.le]
[contravariant_class α α (function.swap has_add.add) has_le.le]
{a b : α} :
@[simp]
theorem
mul_le_iff_le_one_left'
{α : Type u_1}
[mul_one_class α]
[has_le α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
[contravariant_class α α (function.swap has_mul.mul) has_le.le]
{a b : α} :
theorem
exists_square_le
{α : Type u_1}
[mul_one_class α]
[linear_order α]
[covariant_class α α has_mul.mul has_lt.lt]
(a : α) :
theorem
lt_add_of_pos_right
{α : Type u_1}
[add_zero_class α]
[has_lt α]
[covariant_class α α has_add.add has_lt.lt]
(a : α)
{b : α}
(h : 0 < b) :
theorem
lt_mul_of_one_lt_right'
{α : Type u_1}
[mul_one_class α]
[has_lt α]
[covariant_class α α has_mul.mul has_lt.lt]
(a : α)
{b : α}
(h : 1 < b) :
@[simp]
theorem
lt_add_iff_pos_right
{α : Type u_1}
[add_zero_class α]
[has_lt α]
[covariant_class α α has_add.add has_lt.lt]
[contravariant_class α α has_add.add has_lt.lt]
(a : α)
{b : α} :
@[simp]
theorem
lt_mul_iff_one_lt_right'
{α : Type u_1}
[mul_one_class α]
[has_lt α]
[covariant_class α α has_mul.mul has_lt.lt]
[contravariant_class α α has_mul.mul has_lt.lt]
(a : α)
{b : α} :
@[simp]
theorem
add_lt_iff_neg_left
{α : Type u_1}
[add_zero_class α]
[has_lt α]
[covariant_class α α has_add.add has_lt.lt]
[contravariant_class α α has_add.add has_lt.lt]
{a b : α} :
@[simp]
theorem
mul_lt_iff_lt_one_left'
{α : Type u_1}
[mul_one_class α]
[has_lt α]
[covariant_class α α has_mul.mul has_lt.lt]
[contravariant_class α α has_mul.mul has_lt.lt]
{a b : α} :
@[simp]
theorem
lt_add_iff_pos_left
{α : Type u_1}
[add_zero_class α]
[has_lt α]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
[contravariant_class α α (function.swap has_add.add) has_lt.lt]
(a : α)
{b : α} :
@[simp]
theorem
lt_mul_iff_one_lt_left'
{α : Type u_1}
[mul_one_class α]
[has_lt α]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
[contravariant_class α α (function.swap has_mul.mul) has_lt.lt]
(a : α)
{b : α} :
@[simp]
theorem
add_lt_iff_neg_right
{α : Type u_1}
[add_zero_class α]
[has_lt α]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
[contravariant_class α α (function.swap has_add.add) has_lt.lt]
{a : α}
(b : α) :
@[simp]
theorem
mul_lt_iff_lt_one_right'
{α : Type u_1}
[mul_one_class α]
[has_lt α]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
[contravariant_class α α (function.swap has_mul.mul) has_lt.lt]
{a : α}
(b : α) :
theorem
mul_le_of_le_of_le_one
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{a b c : α}
(hbc : b ≤ c)
(ha : a ≤ 1) :
theorem
add_le_of_le_of_nonpos
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
{a b c : α}
(hbc : b ≤ c)
(ha : a ≤ 0) :
theorem
mul_le_one'
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{a b c : α}
(hbc : b ≤ c)
(ha : a ≤ 1) :
Alias of mul_le_of_le_of_le_one.
theorem
add_nonpos
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
{a b c : α}
(hbc : b ≤ c)
(ha : a ≤ 0) :
Alias of add_le_of_le_of_nonpos.
theorem
lt_mul_of_lt_of_one_le
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{a b c : α}
(hbc : b < c)
(ha : 1 ≤ a) :
theorem
lt_add_of_lt_of_nonneg
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
{a b c : α}
(hbc : b < c)
(ha : 0 ≤ a) :
theorem
add_lt_of_lt_of_nonpos
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
{a b c : α}
(hbc : b < c)
(ha : a ≤ 0) :
theorem
mul_lt_of_lt_of_le_one
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{a b c : α}
(hbc : b < c)
(ha : a ≤ 1) :
theorem
lt_add_of_le_of_pos
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_lt.lt]
{a b c : α}
(hbc : b ≤ c)
(ha : 0 < a) :
theorem
lt_mul_of_le_of_one_lt
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_lt.lt]
{a b c : α}
(hbc : b ≤ c)
(ha : 1 < a) :
theorem
mul_lt_of_le_one_of_lt
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b c : α}
(ha : a ≤ 1)
(hb : b < c) :
theorem
add_lt_of_nonpos_of_lt
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b c : α}
(ha : a ≤ 0)
(hb : b < c) :
theorem
add_le_of_nonpos_of_le
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b c : α}
(ha : a ≤ 0)
(hbc : b ≤ c) :
theorem
mul_le_of_le_one_of_le
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b c : α}
(ha : a ≤ 1)
(hbc : b ≤ c) :
theorem
le_add_of_nonneg_of_le
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b c : α}
(ha : 0 ≤ a)
(hbc : b ≤ c) :
theorem
le_mul_of_one_le_of_le
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b c : α}
(ha : 1 ≤ a)
(hbc : b ≤ c) :
theorem
left.mul_lt_one
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_lt.lt]
{a b : α}
(ha : a < 1)
(hb : b < 1) :
Assumes left covariance. The lemma assuming right covariance is right.mul_lt_one.
theorem
left.add_neg
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_lt.lt]
{a b : α}
(ha : a < 0)
(hb : b < 0) :
Assumes left covariance. The lemma assuming right covariance is right.add_neg.
theorem
right.add_neg
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
{a b : α}
(ha : a < 0)
(hb : b < 0) :
Assumes right covariance. The lemma assuming left covariance is left.add_neg
theorem
right.mul_lt_one
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
{a b : α}
(ha : a < 1)
(hb : b < 1) :
Assumes right covariance. The lemma assuming left covariance is left.mul_lt_one.
theorem
add_lt_of_le_of_neg
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_lt.lt]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b c : α}
(hbc : b ≤ c)
(ha : a < 0) :
theorem
mul_lt_of_le_of_lt_one
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_lt.lt]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b c : α}
(hbc : b ≤ c)
(ha : a < 1) :
theorem
mul_lt_of_lt_one_of_le
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
{a b c : α}
(ha : a < 1)
(hbc : b ≤ c) :
theorem
add_lt_of_neg_of_le
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
{a b c : α}
(ha : a < 0)
(hbc : b ≤ c) :
theorem
lt_add_of_pos_of_le
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
{a b c : α}
(ha : 0 < a)
(hbc : b ≤ c) :
theorem
lt_mul_of_one_lt_of_le
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
{a b c : α}
(ha : 1 < a)
(hbc : b ≤ c) :
theorem
le_mul_of_le_of_le_one
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{a b c : α}
(ha : c ≤ a)
(hb : 1 ≤ b) :
Assumes left covariance.
theorem
le_add_of_le_of_nonpos
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
{a b c : α}
(ha : c ≤ a)
(hb : 0 ≤ b) :
Assumes left covariance.
theorem
one_le_mul
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{a b : α}
(ha : 1 ≤ a)
(hb : 1 ≤ b) :
theorem
add_nonneg
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
{a b : α}
(ha : 0 ≤ a)
(hb : 0 ≤ b) :
theorem
lt_mul_of_lt_of_one_lt
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_lt.lt]
{a b c : α}
(ha : c < a)
(hb : 1 < b) :
Assumes left covariance.
theorem
lt_add_of_lt_of_pos
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_lt.lt]
{a b c : α}
(ha : c < a)
(hb : 0 < b) :
Assumes left covariance.
theorem
mul_lt_of_lt_of_lt_one
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_lt.lt]
{a b c : α}
(ha : a < c)
(hb : b < 1) :
Assumes left covariance.
theorem
add_lt_of_lt_of_neg
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_lt.lt]
{a b c : α}
(ha : a < c)
(hb : b < 0) :
Assumes left covariance.
theorem
add_lt_of_neg_of_lt
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
{a b c : α}
(ha : a < 0)
(hb : b < c) :
Assumes right covariance.
theorem
mul_lt_of_lt_one_of_lt
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
{a b c : α}
(ha : a < 1)
(hb : b < c) :
Assumes right covariance.
theorem
right.add_nonneg
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b : α}
(ha : 0 ≤ a)
(hb : 0 ≤ b) :
Assumes right covariance.
theorem
right.one_le_mul
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b : α}
(ha : 1 ≤ a)
(hb : 1 ≤ b) :
Assumes right covariance.
theorem
right.add_pos
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
{b : α}
(hb : 0 < b)
{a : α}
(ha : 0 < a) :
Assumes right covariance.
theorem
right.one_lt_mul
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
{b : α}
(hb : 1 < b)
{a : α}
(ha : 1 < a) :
Assumes right covariance.
theorem
le_add_of_nonneg_right
{α : Type u_1}
[add_zero_class α]
[has_le α]
[covariant_class α α has_add.add has_le.le]
{a b : α}
(h : 0 ≤ b) :
theorem
le_mul_of_one_le_right'
{α : Type u_1}
[mul_one_class α]
[has_le α]
[covariant_class α α has_mul.mul has_le.le]
{a b : α}
(h : 1 ≤ b) :
theorem
mul_le_of_le_one_right'
{α : Type u_1}
[mul_one_class α]
[has_le α]
[covariant_class α α has_mul.mul has_le.le]
{a b : α}
(h : b ≤ 1) :
theorem
add_le_of_nonpos_right
{α : Type u_1}
[add_zero_class α]
[has_le α]
[covariant_class α α has_add.add has_le.le]
{a b : α}
(h : b ≤ 0) :
theorem
add_left_cancel''
{α : Type u_1}
[has_add α]
[partial_order α]
[contravariant_class α α has_add.add has_le.le]
{a b c : α}
(h : a + b = a + c) :
b = c
theorem
mul_left_cancel''
{α : Type u_1}
[has_mul α]
[partial_order α]
[contravariant_class α α has_mul.mul has_le.le]
{a b c : α}
(h : a * b = a * c) :
b = c
theorem
add_right_cancel''
{α : Type u_1}
[has_add α]
[partial_order α]
[contravariant_class α α (function.swap has_add.add) has_le.le]
{a b c : α}
(h : a + b = c + b) :
a = c
theorem
mul_right_cancel''
{α : Type u_1}
[has_mul α]
[partial_order α]
[contravariant_class α α (function.swap has_mul.mul) has_le.le]
{a b c : α}
(h : a * b = c * b) :
a = c
def
contravariant.to_left_cancel_semigroup
{α : Type u_1}
[semigroup α]
[partial_order α]
[contravariant_class α α has_mul.mul has_le.le] :
A semigroup with a partial order and satisfying left_cancel_semigroup
(i.e. a * c < b * c → a < b) is a left_cancel semigroup.
Equations
- contravariant.to_left_cancel_semigroup = {mul := semigroup.mul _inst_1, mul_assoc := _, mul_left_cancel := _}
def
contravariant.to_left_cancel_add_semigroup
{α : Type u_1}
[add_semigroup α]
[partial_order α]
[contravariant_class α α has_add.add has_le.le] :
An additive semigroup with a partial order and satisfying left_cancel_add_semigroup
(i.e. c + a < c + b → a < b) is a left_cancel add_semigroup.
Equations
- contravariant.to_left_cancel_add_semigroup = {add := add_semigroup.add _inst_1, add_assoc := _, add_left_cancel := _}
def
contravariant.to_right_cancel_add_semigroup
{α : Type u_1}
[add_semigroup α]
[partial_order α]
[contravariant_class α α (function.swap has_add.add) has_le.le] :
An additive semigroup with a partial order and satisfying right_cancel_add_semigroup
(a + c < b + c → a < b) is a right_cancel add_semigroup.
Equations
- contravariant.to_right_cancel_add_semigroup = {add := add_semigroup.add _inst_1, add_assoc := _, add_right_cancel := _}
def
contravariant.to_right_cancel_semigroup
{α : Type u_1}
[semigroup α]
[partial_order α]
[contravariant_class α α (function.swap has_mul.mul) has_le.le] :
A semigroup with a partial order and satisfying right_cancel_semigroup
(i.e. a * c < b * c → a < b) is a right_cancel semigroup.
Equations
- contravariant.to_right_cancel_semigroup = {mul := semigroup.mul _inst_1, mul_assoc := _, mul_right_cancel := _}
theorem
mul_lt_mul_of_lt_of_lt
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_mul α]
[covariant_class α α has_mul.mul has_lt.lt]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
(h₁ : a < b)
(h₂ : c < d) :
theorem
add_lt_add_of_lt_of_lt
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_add α]
[covariant_class α α has_add.add has_lt.lt]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
(h₁ : a < b)
(h₂ : c < d) :
theorem
mul_lt_mul_of_le_of_lt
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_mul α]
[covariant_class α α has_mul.mul has_lt.lt]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(h₁ : a ≤ b)
(h₂ : c < d) :
theorem
add_lt_add_of_le_of_lt
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_add α]
[covariant_class α α has_add.add has_lt.lt]
[covariant_class α α (function.swap has_add.add) has_le.le]
(h₁ : a ≤ b)
(h₂ : c < d) :
theorem
mul_lt_mul'''
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_mul α]
[covariant_class α α has_mul.mul has_lt.lt]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(h₁ : a < b)
(h₂ : c < d) :
theorem
add_lt_add
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_add α]
[covariant_class α α has_add.add has_lt.lt]
[covariant_class α α (function.swap has_add.add) has_le.le]
(h₁ : a < b)
(h₂ : c < d) :
theorem
add_eq_add_iff_eq_and_eq
{α : Type u_1}
[add_semigroup α]
[partial_order α]
[contravariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
[covariant_class α α has_add.add has_lt.lt]
[contravariant_class α α (function.swap has_add.add) has_le.le]
{a b c d : α}
(hac : a ≤ c)
(hbd : b ≤ d) :
theorem
mul_eq_mul_iff_eq_and_eq
{α : Type u_1}
[semigroup α]
[partial_order α]
[contravariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
[covariant_class α α has_mul.mul has_lt.lt]
[contravariant_class α α (function.swap has_mul.mul) has_le.le]
{a b c d : α}
(hac : a ≤ c)
(hbd : b ≤ d) :
theorem
mul_lt_of_mul_lt_left
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_mul α]
[covariant_class α α has_mul.mul has_le.le]
(h : a * b < c)
(hle : d ≤ b) :
theorem
add_lt_of_add_lt_left
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_add α]
[covariant_class α α has_add.add has_le.le]
(h : a + b < c)
(hle : d ≤ b) :
theorem
add_le_of_add_le_left
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_add α]
[covariant_class α α has_add.add has_le.le]
(h : a + b ≤ c)
(hle : d ≤ b) :
theorem
mul_le_of_mul_le_left
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_mul α]
[covariant_class α α has_mul.mul has_le.le]
(h : a * b ≤ c)
(hle : d ≤ b) :
theorem
lt_add_of_lt_add_left
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_add α]
[covariant_class α α has_add.add has_le.le]
(h : a < b + c)
(hle : c ≤ d) :
theorem
lt_mul_of_lt_mul_left
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_mul α]
[covariant_class α α has_mul.mul has_le.le]
(h : a < b * c)
(hle : c ≤ d) :
theorem
le_add_of_le_add_left
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_add α]
[covariant_class α α has_add.add has_le.le]
(h : a ≤ b + c)
(hle : c ≤ d) :
theorem
le_mul_of_le_mul_left
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_mul α]
[covariant_class α α has_mul.mul has_le.le]
(h : a ≤ b * c)
(hle : c ≤ d) :
theorem
add_lt_add_of_lt_of_le
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_add α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
(h₁ : a < b)
(h₂ : c ≤ d) :
theorem
mul_lt_mul_of_lt_of_le
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_mul α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
(h₁ : a < b)
(h₂ : c ≤ d) :
Here we start using properties of one, on the left.
theorem
lt_of_mul_lt_of_one_le_left
{α : Type u_1}
{a b c : α}
[preorder α]
[mul_one_class α]
[covariant_class α α has_mul.mul has_le.le]
(h : a * b < c)
(hle : 1 ≤ b) :
a < c
theorem
lt_of_add_lt_of_nonneg_left
{α : Type u_1}
{a b c : α}
[preorder α]
[add_zero_class α]
[covariant_class α α has_add.add has_le.le]
(h : a + b < c)
(hle : 0 ≤ b) :
a < c
theorem
le_of_mul_le_of_one_le_left
{α : Type u_1}
{a b c : α}
[preorder α]
[mul_one_class α]
[covariant_class α α has_mul.mul has_le.le]
(h : a * b ≤ c)
(hle : 1 ≤ b) :
a ≤ c
theorem
le_of_add_le_of_nonneg_left
{α : Type u_1}
{a b c : α}
[preorder α]
[add_zero_class α]
[covariant_class α α has_add.add has_le.le]
(h : a + b ≤ c)
(hle : 0 ≤ b) :
a ≤ c
theorem
lt_of_lt_add_of_nonpos_left
{α : Type u_1}
{a b c : α}
[preorder α]
[add_zero_class α]
[covariant_class α α has_add.add has_le.le]
(h : a < b + c)
(hle : c ≤ 0) :
a < b
theorem
lt_of_lt_mul_of_le_one_left
{α : Type u_1}
{a b c : α}
[preorder α]
[mul_one_class α]
[covariant_class α α has_mul.mul has_le.le]
(h : a < b * c)
(hle : c ≤ 1) :
a < b
theorem
le_of_le_add_of_nonpos_left
{α : Type u_1}
{a b c : α}
[preorder α]
[add_zero_class α]
[covariant_class α α has_add.add has_le.le]
(h : a ≤ b + c)
(hle : c ≤ 0) :
a ≤ b
theorem
le_of_le_mul_of_le_one_left
{α : Type u_1}
{a b c : α}
[preorder α]
[mul_one_class α]
[covariant_class α α has_mul.mul has_le.le]
(h : a ≤ b * c)
(hle : c ≤ 1) :
a ≤ b
theorem
mul_lt_of_mul_lt_right
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_mul α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(h : a * b < c)
(hle : d ≤ a) :
theorem
add_lt_of_add_lt_right
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_add α]
[covariant_class α α (function.swap has_add.add) has_le.le]
(h : a + b < c)
(hle : d ≤ a) :
theorem
mul_le_of_mul_le_right
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_mul α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(h : a * b ≤ c)
(hle : d ≤ a) :
theorem
add_le_of_add_le_right
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_add α]
[covariant_class α α (function.swap has_add.add) has_le.le]
(h : a + b ≤ c)
(hle : d ≤ a) :
theorem
lt_add_of_lt_add_right
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_add α]
[covariant_class α α (function.swap has_add.add) has_le.le]
(h : a < b + c)
(hle : b ≤ d) :
theorem
lt_mul_of_lt_mul_right
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_mul α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(h : a < b * c)
(hle : b ≤ d) :
theorem
le_mul_of_le_mul_right
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_mul α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(h : a ≤ b * c)
(hle : b ≤ d) :
theorem
le_add_of_le_add_right
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_add α]
[covariant_class α α (function.swap has_add.add) has_le.le]
(h : a ≤ b + c)
(hle : b ≤ d) :
theorem
add_le_add
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_add α]
[covariant_class α α (function.swap has_add.add) has_le.le]
[covariant_class α α has_add.add has_le.le]
(h₁ : a ≤ b)
(h₂ : c ≤ d) :
theorem
mul_le_mul'
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_mul α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
[covariant_class α α has_mul.mul has_le.le]
(h₁ : a ≤ b)
(h₂ : c ≤ d) :
theorem
mul_le_mul_three
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_mul α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
[covariant_class α α has_mul.mul has_le.le]
{e f : α}
(h₁ : a ≤ d)
(h₂ : b ≤ e)
(h₃ : c ≤ f) :
theorem
add_le_add_three
{α : Type u_1}
{a b c d : α}
[preorder α]
[has_add α]
[covariant_class α α (function.swap has_add.add) has_le.le]
[covariant_class α α has_add.add has_le.le]
{e f : α}
(h₁ : a ≤ d)
(h₂ : b ≤ e)
(h₃ : c ≤ f) :
Here we start using properties of one, on the right.
theorem
le_mul_of_one_le_left'
{α : Type u_1}
{a b : α}
[preorder α]
[mul_one_class α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(h : 1 ≤ b) :
theorem
le_add_of_nonneg_left
{α : Type u_1}
{a b : α}
[preorder α]
[add_zero_class α]
[covariant_class α α (function.swap has_add.add) has_le.le]
(h : 0 ≤ b) :
theorem
add_le_of_nonpos_left
{α : Type u_1}
{a b : α}
[preorder α]
[add_zero_class α]
[covariant_class α α (function.swap has_add.add) has_le.le]
(h : b ≤ 0) :
theorem
mul_le_of_le_one_left'
{α : Type u_1}
{a b : α}
[preorder α]
[mul_one_class α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(h : b ≤ 1) :
theorem
lt_of_mul_lt_of_one_le_right
{α : Type u_1}
{a b c : α}
[preorder α]
[mul_one_class α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(h : a * b < c)
(hle : 1 ≤ a) :
b < c
theorem
lt_of_add_lt_of_nonneg_right
{α : Type u_1}
{a b c : α}
[preorder α]
[add_zero_class α]
[covariant_class α α (function.swap has_add.add) has_le.le]
(h : a + b < c)
(hle : 0 ≤ a) :
b < c
theorem
le_of_mul_le_of_one_le_right
{α : Type u_1}
{a b c : α}
[preorder α]
[mul_one_class α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(h : a * b ≤ c)
(hle : 1 ≤ a) :
b ≤ c
theorem
le_of_add_le_of_nonneg_right
{α : Type u_1}
{a b c : α}
[preorder α]
[add_zero_class α]
[covariant_class α α (function.swap has_add.add) has_le.le]
(h : a + b ≤ c)
(hle : 0 ≤ a) :
b ≤ c
theorem
lt_of_lt_add_of_nonpos_right
{α : Type u_1}
{a b c : α}
[preorder α]
[add_zero_class α]
[covariant_class α α (function.swap has_add.add) has_le.le]
(h : a < b + c)
(hle : b ≤ 0) :
a < c
theorem
lt_of_lt_mul_of_le_one_right
{α : Type u_1}
{a b c : α}
[preorder α]
[mul_one_class α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(h : a < b * c)
(hle : b ≤ 1) :
a < c
theorem
le_of_le_mul_of_le_one_right
{α : Type u_1}
{a b c : α}
[preorder α]
[mul_one_class α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(h : a ≤ b * c)
(hle : b ≤ 1) :
a ≤ c
theorem
le_of_le_add_of_nonpos_right
{α : Type u_1}
{a b c : α}
[preorder α]
[add_zero_class α]
[covariant_class α α (function.swap has_add.add) has_le.le]
(h : a ≤ b + c)
(hle : b ≤ 0) :
a ≤ c
theorem
lt_add_of_pos_left
{α : Type u_1}
[preorder α]
[add_zero_class α]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
(a : α)
{b : α}
(h : 0 < b) :
theorem
lt_mul_of_one_lt_left'
{α : Type u_1}
[preorder α]
[mul_one_class α]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
(a : α)
{b : α}
(h : 1 < b) :
theorem
one_lt_mul_of_lt_of_le'
{α : Type u_1}
{a b : α}
[preorder α]
[mul_one_class α]
[covariant_class α α has_mul.mul has_le.le]
(ha : 1 < a)
(hb : 1 ≤ b) :
theorem
add_pos_of_pos_of_nonneg
{α : Type u_1}
{a b : α}
[preorder α]
[add_zero_class α]
[covariant_class α α has_add.add has_le.le]
(ha : 0 < a)
(hb : 0 ≤ b) :
theorem
one_lt_mul'
{α : Type u_1}
{a b : α}
[preorder α]
[mul_one_class α]
[covariant_class α α has_mul.mul has_le.le]
(ha : 1 < a)
(hb : 1 < b) :
theorem
add_pos
{α : Type u_1}
{a b : α}
[preorder α]
[add_zero_class α]
[covariant_class α α has_add.add has_le.le]
(ha : 0 < a)
(hb : 0 < b) :
theorem
lt_mul_of_lt_of_one_le'
{α : Type u_1}
{a b c : α}
[preorder α]
[mul_one_class α]
[covariant_class α α has_mul.mul has_le.le]
(hbc : b < c)
(ha : 1 ≤ a) :
theorem
lt_add_of_lt_of_nonneg'
{α : Type u_1}
{a b c : α}
[preorder α]
[add_zero_class α]
[covariant_class α α has_add.add has_le.le]
(hbc : b < c)
(ha : 0 ≤ a) :
theorem
lt_add_of_lt_of_pos'
{α : Type u_1}
{a b c : α}
[preorder α]
[add_zero_class α]
[covariant_class α α has_add.add has_le.le]
(hbc : b < c)
(ha : 0 < a) :
theorem
lt_mul_of_lt_of_one_lt'
{α : Type u_1}
{a b c : α}
[preorder α]
[mul_one_class α]
[covariant_class α α has_mul.mul has_le.le]
(hbc : b < c)
(ha : 1 < a) :
theorem
le_add_of_le_of_nonneg
{α : Type u_1}
{a b c : α}
[preorder α]
[add_zero_class α]
[covariant_class α α has_add.add has_le.le]
(hbc : b ≤ c)
(ha : 0 ≤ a) :
theorem
le_mul_of_le_of_one_le
{α : Type u_1}
{a b c : α}
[preorder α]
[mul_one_class α]
[covariant_class α α has_mul.mul has_le.le]
(hbc : b ≤ c)
(ha : 1 ≤ a) :
theorem
one_le_mul_right
{α : Type u_1}
{a b : α}
[preorder α]
[mul_one_class α]
[covariant_class α α has_mul.mul has_le.le]
(ha : 1 ≤ a)
(hb : 1 ≤ b) :
theorem
add_pos_of_nonneg_of_pos
{α : Type u_1}
{a b : α}
[preorder α]
[add_zero_class α]
[covariant_class α α (function.swap has_add.add) has_le.le]
(ha : 0 ≤ a)
(hb : 0 < b) :
theorem
one_lt_mul_of_le_of_lt'
{α : Type u_1}
{a b : α}
[preorder α]
[mul_one_class α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(ha : 1 ≤ a)
(hb : 1 < b) :
theorem
lt_mul_of_one_le_of_lt
{α : Type u_1}
{a b c : α}
[preorder α]
[mul_one_class α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(ha : 1 ≤ a)
(hbc : b < c) :
theorem
lt_add_of_nonneg_of_lt
{α : Type u_1}
{a b c : α}
[preorder α]
[add_zero_class α]
[covariant_class α α (function.swap has_add.add) has_le.le]
(ha : 0 ≤ a)
(hbc : b < c) :
theorem
lt_mul_of_one_lt_of_lt
{α : Type u_1}
{a b c : α}
[preorder α]
[mul_one_class α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(ha : 1 < a)
(hbc : b < c) :
theorem
lt_add_of_pos_of_lt
{α : Type u_1}
{a b c : α}
[preorder α]
[add_zero_class α]
[covariant_class α α (function.swap has_add.add) has_le.le]
(ha : 0 < a)
(hbc : b < c) :
Properties assuming partial_order.
theorem
add_eq_zero_iff'
{α : Type u_1}
{a b : α}
[add_zero_class α]
[partial_order α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(ha : 0 ≤ a)
(hb : 0 ≤ b) :
theorem
mul_eq_one_iff'
{α : Type u_1}
{a b : α}
[mul_one_class α]
[partial_order α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(ha : 1 ≤ a)
(hb : 1 ≤ b) :
theorem
monotone.const_add
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f : β → α}
[covariant_class α α has_add.add has_le.le]
(hf : monotone f)
(a : α) :
theorem
monotone.const_mul'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f : β → α}
[covariant_class α α has_mul.mul has_le.le]
(hf : monotone f)
(a : α) :
theorem
monotone.add_const
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f : β → α}
[covariant_class α α (function.swap has_add.add) has_le.le]
(hf : monotone f)
(a : α) :
theorem
monotone.mul_const'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f : β → α}
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(hf : monotone f)
(a : α) :
theorem
monotone.mul'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f g : β → α}
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(hf : monotone f)
(hg : monotone g) :
The product of two monotone functions is monotone.
theorem
monotone.add
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f g : β → α}
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(hf : monotone f)
(hg : monotone g) :
The sum of two monotone functions is monotone.
theorem
strict_mono.const_add
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f : β → α}
[covariant_class α α has_add.add has_lt.lt]
(hf : strict_mono f)
(c : α) :
strict_mono (λ (x : β), c + f x)
theorem
strict_mono.const_mul'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f : β → α}
[covariant_class α α has_mul.mul has_lt.lt]
(hf : strict_mono f)
(c : α) :
strict_mono (λ (x : β), c * f x)
theorem
strict_mono.add_const
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f : β → α}
[covariant_class α α (function.swap has_add.add) has_lt.lt]
(hf : strict_mono f)
(c : α) :
strict_mono (λ (x : β), f x + c)
theorem
strict_mono.mul_const'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f : β → α}
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
(hf : strict_mono f)
(c : α) :
strict_mono (λ (x : β), (f x) * c)
theorem
strict_mono.mul'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f g : β → α}
[covariant_class α α has_mul.mul has_lt.lt]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
(hf : strict_mono f)
(hg : strict_mono g) :
strict_mono (λ (x : β), (f x) * g x)
The product of two strictly monotone functions is strictly monotone.
theorem
strict_mono.add
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f g : β → α}
[covariant_class α α has_add.add has_lt.lt]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
(hf : strict_mono f)
(hg : strict_mono g) :
strict_mono (λ (x : β), f x + g x)
The sum of two strictly monotone functions is strictly monotone.
theorem
monotone.mul_strict_mono'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
[covariant_class α α has_mul.mul has_lt.lt]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{f g : β → α}
(hf : monotone f)
(hg : strict_mono g) :
strict_mono (λ (x : β), (f x) * g x)
The product of a monotone function and a strictly monotone function is strictly monotone.
theorem
monotone.add_strict_mono
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
[covariant_class α α has_add.add has_lt.lt]
[covariant_class α α (function.swap has_add.add) has_le.le]
{f g : β → α}
(hf : monotone f)
(hg : strict_mono g) :
strict_mono (λ (x : β), f x + g x)
The sum of a monotone function and a strictly monotone function is strictly monotone.
theorem
strict_mono.add_monotone
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f g : β → α}
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
(hf : strict_mono f)
(hg : monotone g) :
strict_mono (λ (x : β), f x + g x)
The sum of a strictly monotone function and a monotone function is strictly monotone.
theorem
strict_mono.mul_monotone'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f g : β → α}
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
(hf : strict_mono f)
(hg : monotone g) :
strict_mono (λ (x : β), (f x) * g x)
The product of a strictly monotone function and a monotone function is strictly monotone.
An element a : α is add_le_cancellable if x ↦ a + x is order-reflecting.
We will make a separate version of many lemmas that require [contravariant_class α α (+) (≤)] with
mul_le_cancellable assumptions instead. These lemmas can then be instantiated to specific types,
like ennreal, where we can replace the assumption add_le_cancellable x by x ≠ ∞.
An element a : α is mul_le_cancellable if x ↦ a * x is order-reflecting.
We will make a separate version of many lemmas that require [contravariant_class α α (*) (≤)] with
mul_le_cancellable assumptions instead. These lemmas can then be instantiated to specific types,
like ennreal, where we can replace the assumption add_le_cancellable x by x ≠ ∞.
theorem
contravariant.add_le_cancellable
{α : Type u_1}
[has_add α]
[has_le α]
[contravariant_class α α has_add.add has_le.le]
{a : α} :
theorem
contravariant.mul_le_cancellable
{α : Type u_1}
[has_mul α]
[has_le α]
[contravariant_class α α has_mul.mul has_le.le]
{a : α} :
@[protected]
theorem
mul_le_cancellable.injective
{α : Type u_1}
[has_mul α]
[partial_order α]
{a : α}
(ha : mul_le_cancellable a) :
@[protected]
theorem
add_le_cancellable.injective
{α : Type u_1}
[has_add α]
[partial_order α]
{a : α}
(ha : add_le_cancellable a) :
@[protected]
theorem
mul_le_cancellable.inj
{α : Type u_1}
[has_mul α]
[partial_order α]
{a b c : α}
(ha : mul_le_cancellable a) :
@[protected]
theorem
add_le_cancellable.inj
{α : Type u_1}
[has_add α]
[partial_order α]
{a b c : α}
(ha : add_le_cancellable a) :
@[protected]
theorem
add_le_cancellable.injective_left
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
{a : α}
(ha : add_le_cancellable a) :
function.injective (λ (_x : α), _x + a)
@[protected]
theorem
mul_le_cancellable.injective_left
{α : Type u_1}
[comm_semigroup α]
[partial_order α]
{a : α}
(ha : mul_le_cancellable a) :
function.injective (λ (_x : α), _x * a)
@[protected]
theorem
add_le_cancellable.inj_left
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
{a b c : α}
(hc : add_le_cancellable c) :
@[protected]
theorem
mul_le_cancellable.inj_left
{α : Type u_1}
[comm_semigroup α]
[partial_order α]
{a b c : α}
(hc : mul_le_cancellable c) :
@[protected]
theorem
mul_le_cancellable.mul_le_mul_iff_left
{α : Type u_1}
[has_le α]
[has_mul α]
[covariant_class α α has_mul.mul has_le.le]
{a b c : α}
(ha : mul_le_cancellable a) :
@[protected]
theorem
add_le_cancellable.add_le_add_iff_left
{α : Type u_1}
[has_le α]
[has_add α]
[covariant_class α α has_add.add has_le.le]
{a b c : α}
(ha : add_le_cancellable a) :
@[protected]
theorem
mul_le_cancellable.mul_le_mul_iff_right
{α : Type u_1}
[has_le α]
[comm_semigroup α]
[covariant_class α α has_mul.mul has_le.le]
{a b c : α}
(ha : mul_le_cancellable a) :
@[protected]
theorem
add_le_cancellable.add_le_add_iff_right
{α : Type u_1}
[has_le α]
[add_comm_semigroup α]
[covariant_class α α has_add.add has_le.le]
{a b c : α}
(ha : add_le_cancellable a) :
@[protected]
theorem
add_le_cancellable.le_add_iff_nonneg_right
{α : Type u_1}
[has_le α]
[add_zero_class α]
[covariant_class α α has_add.add has_le.le]
{a b : α}
(ha : add_le_cancellable a) :
@[protected]
theorem
mul_le_cancellable.le_mul_iff_one_le_right
{α : Type u_1}
[has_le α]
[mul_one_class α]
[covariant_class α α has_mul.mul has_le.le]
{a b : α}
(ha : mul_le_cancellable a) :
@[protected]
theorem
mul_le_cancellable.mul_le_iff_le_one_right
{α : Type u_1}
[has_le α]
[mul_one_class α]
[covariant_class α α has_mul.mul has_le.le]
{a b : α}
(ha : mul_le_cancellable a) :
@[protected]
theorem
add_le_cancellable.add_le_iff_nonpos_right
{α : Type u_1}
[has_le α]
[add_zero_class α]
[covariant_class α α has_add.add has_le.le]
{a b : α}
(ha : add_le_cancellable a) :
@[protected]
theorem
add_le_cancellable.le_add_iff_nonneg_left
{α : Type u_1}
[has_le α]
[add_comm_monoid α]
[covariant_class α α has_add.add has_le.le]
{a b : α}
(ha : add_le_cancellable a) :
@[protected]
theorem
mul_le_cancellable.le_mul_iff_one_le_left
{α : Type u_1}
[has_le α]
[comm_monoid α]
[covariant_class α α has_mul.mul has_le.le]
{a b : α}
(ha : mul_le_cancellable a) :
@[protected]
theorem
add_le_cancellable.add_le_iff_nonpos_left
{α : Type u_1}
[has_le α]
[add_comm_monoid α]
[covariant_class α α has_add.add has_le.le]
{a b : α}
(ha : add_le_cancellable a) :
@[protected]
theorem
mul_le_cancellable.mul_le_iff_le_one_left
{α : Type u_1}
[has_le α]
[comm_monoid α]
[covariant_class α α has_mul.mul has_le.le]
{a b : α}
(ha : mul_le_cancellable a) :