Ordered monoids #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
theorem
mul_lt_mul_of_lt_of_lt
{α : Type u_1}
[has_mul α]
[preorder α]
[covariant_class α α has_mul.mul has_lt.lt]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
{a b c d : α}
(h₁ : a < b)
(h₂ : c < d) :
theorem
add_lt_add_of_lt_of_lt
{α : Type u_1}
[has_add α]
[preorder α]
[covariant_class α α has_add.add has_lt.lt]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
{a b c d : α}
(h₁ : a < b)
(h₂ : c < d) :
theorem
add_lt_add
{α : Type u_1}
[has_add α]
[preorder α]
[covariant_class α α has_add.add has_lt.lt]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
{a b c d : α}
(h₁ : a < b)
(h₂ : c < d) :
Alias of add_lt_add_of_lt_of_lt.
theorem
mul_lt_mul_of_le_of_lt
{α : Type u_1}
[has_mul α]
[preorder α]
[covariant_class α α has_mul.mul has_lt.lt]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b c d : α}
(h₁ : a ≤ b)
(h₂ : c < d) :
theorem
add_lt_add_of_le_of_lt
{α : Type u_1}
[has_add α]
[preorder α]
[covariant_class α α has_add.add has_lt.lt]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b c d : α}
(h₁ : a ≤ b)
(h₂ : c < d) :
theorem
add_lt_add_of_lt_of_le
{α : Type u_1}
[has_add α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
{a b c d : α}
(h₁ : a < b)
(h₂ : c ≤ d) :
theorem
mul_lt_mul_of_lt_of_le
{α : Type u_1}
[has_mul α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
{a b c d : α}
(h₁ : a < b)
(h₂ : c ≤ d) :
theorem
left.mul_lt_mul
{α : Type u_1}
[has_mul α]
[preorder α]
[covariant_class α α has_mul.mul has_lt.lt]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b c d : α}
(h₁ : a < b)
(h₂ : c < d) :
Only assumes left strict covariance.
theorem
left.add_lt_add
{α : Type u_1}
[has_add α]
[preorder α]
[covariant_class α α has_add.add has_lt.lt]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b c d : α}
(h₁ : a < b)
(h₂ : c < d) :
Only assumes left strict covariance
theorem
right.add_lt_add
{α : Type u_1}
[has_add α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
{a b c d : α}
(h₁ : a < b)
(h₂ : c < d) :
Only assumes right strict covariance
theorem
right.mul_lt_mul
{α : Type u_1}
[has_mul α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
{a b c d : α}
(h₁ : a < b)
(h₂ : c < d) :
Only assumes right strict covariance.
theorem
add_le_add
{α : Type u_1}
[has_add α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b c d : α}
(h₁ : a ≤ b)
(h₂ : c ≤ d) :
theorem
mul_le_mul'
{α : Type u_1}
[has_mul α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b c d : α}
(h₁ : a ≤ b)
(h₂ : c ≤ d) :
theorem
mul_le_mul_three
{α : Type u_1}
[has_mul α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b c d e f : α}
(h₁ : a ≤ d)
(h₂ : b ≤ e)
(h₃ : c ≤ f) :
theorem
add_le_add_three
{α : Type u_1}
[has_add α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b c d e f : α}
(h₁ : a ≤ d)
(h₂ : b ≤ e)
(h₃ : c ≤ f) :
theorem
mul_lt_of_mul_lt_left
{α : Type u_1}
[has_mul α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{a b c d : α}
(h : a * b < c)
(hle : d ≤ b) :
theorem
add_lt_of_add_lt_left
{α : Type u_1}
[has_add α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
{a b c d : α}
(h : a + b < c)
(hle : d ≤ b) :
theorem
add_le_of_add_le_left
{α : Type u_1}
[has_add α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
{a b c d : α}
(h : a + b ≤ c)
(hle : d ≤ b) :
theorem
mul_le_of_mul_le_left
{α : Type u_1}
[has_mul α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{a b c d : α}
(h : a * b ≤ c)
(hle : d ≤ b) :
theorem
mul_lt_of_mul_lt_right
{α : Type u_1}
[has_mul α]
[preorder α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b c d : α}
(h : a * b < c)
(hle : d ≤ a) :
theorem
add_lt_of_add_lt_right
{α : Type u_1}
[has_add α]
[preorder α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b c d : α}
(h : a + b < c)
(hle : d ≤ a) :
theorem
mul_le_of_mul_le_right
{α : Type u_1}
[has_mul α]
[preorder α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b c d : α}
(h : a * b ≤ c)
(hle : d ≤ a) :
theorem
add_le_of_add_le_right
{α : Type u_1}
[has_add α]
[preorder α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b c d : α}
(h : a + b ≤ c)
(hle : d ≤ a) :
theorem
lt_add_of_lt_add_left
{α : Type u_1}
[has_add α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
{a b c d : α}
(h : a < b + c)
(hle : c ≤ d) :
theorem
lt_mul_of_lt_mul_left
{α : Type u_1}
[has_mul α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{a b c d : α}
(h : a < b * c)
(hle : c ≤ d) :
theorem
le_add_of_le_add_left
{α : Type u_1}
[has_add α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
{a b c d : α}
(h : a ≤ b + c)
(hle : c ≤ d) :
theorem
le_mul_of_le_mul_left
{α : Type u_1}
[has_mul α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{a b c d : α}
(h : a ≤ b * c)
(hle : c ≤ d) :
theorem
lt_add_of_lt_add_right
{α : Type u_1}
[has_add α]
[preorder α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b c d : α}
(h : a < b + c)
(hle : b ≤ d) :
theorem
lt_mul_of_lt_mul_right
{α : Type u_1}
[has_mul α]
[preorder α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b c d : α}
(h : a < b * c)
(hle : b ≤ d) :
theorem
le_mul_of_le_mul_right
{α : Type u_1}
[has_mul α]
[preorder α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b c d : α}
(h : a ≤ b * c)
(hle : b ≤ d) :
theorem
le_add_of_le_add_right
{α : Type u_1}
[has_add α]
[preorder α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b c d : α}
(h : a ≤ b + c)
(hle : b ≤ d) :
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
theorem
min_le_max_of_mul_le_mul
{α : Type u_1}
[has_mul α]
[linear_order α]
{a b c d : α}
[covariant_class α α has_mul.mul has_lt.lt]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
(h : a * b ≤ c * d) :
linear_order.min a b ≤ linear_order.max c d
theorem
min_le_max_of_add_le_add
{α : Type u_1}
[has_add α]
[linear_order α]
{a b c d : α}
[covariant_class α α has_add.add has_lt.lt]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
(h : a + b ≤ c + d) :
linear_order.min a b ≤ linear_order.max c d
theorem
max_add_add_le_max_add_max
{α : Type u_1}
[has_add α]
[linear_order α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b c d : α} :
linear_order.max (a + b) (c + d) ≤ linear_order.max a c + linear_order.max b d
theorem
max_mul_mul_le_max_mul_max'
{α : Type u_1}
[has_mul α]
[linear_order α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b c d : α} :
linear_order.max (a * b) (c * d) ≤ linear_order.max a c * linear_order.max b d
theorem
min_add_min_le_min_add_add
{α : Type u_1}
[has_add α]
[linear_order α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b c d : α} :
linear_order.min a c + linear_order.min b d ≤ linear_order.min (a + b) (c + d)
theorem
min_mul_min_le_min_mul_mul'
{α : Type u_1}
[has_mul α]
[linear_order α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b c d : α} :
linear_order.min a c * linear_order.min b d ≤ linear_order.min (a * b) (c * d)
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
le_mul_of_one_le_left'
{α : Type u_1}
[mul_one_class α]
[has_le α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b : α}
(h : 1 ≤ b) :
theorem
le_add_of_nonneg_left
{α : Type u_1}
[add_zero_class α]
[has_le α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b : α}
(h : 0 ≤ b) :
theorem
add_le_of_nonpos_left
{α : Type u_1}
[add_zero_class α]
[has_le α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b : α}
(h : b ≤ 0) :
theorem
mul_le_of_le_one_left'
{α : Type u_1}
[mul_one_class α]
[has_le α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b : α}
(h : b ≤ 1) :
theorem
one_le_of_le_mul_right
{α : Type u_1}
[mul_one_class α]
[has_le α]
[contravariant_class α α has_mul.mul has_le.le]
{a b : α}
(h : a ≤ a * b) :
1 ≤ b
theorem
nonneg_of_le_add_right
{α : Type u_1}
[add_zero_class α]
[has_le α]
[contravariant_class α α has_add.add has_le.le]
{a b : α}
(h : a ≤ a + b) :
0 ≤ b
theorem
le_one_of_mul_le_right
{α : Type u_1}
[mul_one_class α]
[has_le α]
[contravariant_class α α has_mul.mul has_le.le]
{a b : α}
(h : a * b ≤ a) :
b ≤ 1
theorem
nonpos_of_add_le_right
{α : Type u_1}
[add_zero_class α]
[has_le α]
[contravariant_class α α has_add.add has_le.le]
{a b : α}
(h : a + b ≤ a) :
b ≤ 0
theorem
nonneg_of_le_add_left
{α : Type u_1}
[add_zero_class α]
[has_le α]
[contravariant_class α α (function.swap has_add.add) has_le.le]
{a b : α}
(h : b ≤ a + b) :
0 ≤ a
theorem
one_le_of_le_mul_left
{α : Type u_1}
[mul_one_class α]
[has_le α]
[contravariant_class α α (function.swap has_mul.mul) has_le.le]
{a b : α}
(h : b ≤ a * b) :
1 ≤ a
theorem
nonpos_of_add_le_left
{α : Type u_1}
[add_zero_class α]
[has_le α]
[contravariant_class α α (function.swap has_add.add) has_le.le]
{a b : α}
(h : a + b ≤ b) :
a ≤ 0
theorem
le_one_of_mul_le_left
{α : Type u_1}
[mul_one_class α]
[has_le α]
[contravariant_class α α (function.swap has_mul.mul) has_le.le]
{a b : α}
(h : a * b ≤ b) :
a ≤ 1
@[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
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_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
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
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) :
theorem
add_lt_of_neg_right
{α : Type u_1}
[add_zero_class α]
[has_lt α]
[covariant_class α α has_add.add has_lt.lt]
(a : α)
{b : α}
(h : b < 0) :
theorem
mul_lt_of_lt_one_right'
{α : Type u_1}
[mul_one_class α]
[has_lt α]
[covariant_class α α has_mul.mul has_lt.lt]
(a : α)
{b : α}
(h : b < 1) :
theorem
lt_add_of_pos_left
{α : Type u_1}
[add_zero_class α]
[has_lt α]
[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}
[mul_one_class α]
[has_lt α]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
(a : α)
{b : α}
(h : 1 < b) :
theorem
add_lt_of_neg_left
{α : Type u_1}
[add_zero_class α]
[has_lt α]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
(a : α)
{b : α}
(h : b < 0) :
theorem
mul_lt_of_lt_one_left'
{α : Type u_1}
[mul_one_class α]
[has_lt α]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
(a : α)
{b : α}
(h : b < 1) :
theorem
pos_of_lt_add_right
{α : Type u_1}
[add_zero_class α]
[has_lt α]
[contravariant_class α α has_add.add has_lt.lt]
{a b : α}
(h : a < a + b) :
0 < b
theorem
one_lt_of_lt_mul_right
{α : Type u_1}
[mul_one_class α]
[has_lt α]
[contravariant_class α α has_mul.mul has_lt.lt]
{a b : α}
(h : a < a * b) :
1 < b
theorem
lt_one_of_mul_lt_right
{α : Type u_1}
[mul_one_class α]
[has_lt α]
[contravariant_class α α has_mul.mul has_lt.lt]
{a b : α}
(h : a * b < a) :
b < 1
theorem
neg_of_add_lt_right
{α : Type u_1}
[add_zero_class α]
[has_lt α]
[contravariant_class α α has_add.add has_lt.lt]
{a b : α}
(h : a + b < a) :
b < 0
theorem
one_lt_of_lt_mul_left
{α : Type u_1}
[mul_one_class α]
[has_lt α]
[contravariant_class α α (function.swap has_mul.mul) has_lt.lt]
{a b : α}
(h : b < a * b) :
1 < a
theorem
pos_of_lt_add_left
{α : Type u_1}
[add_zero_class α]
[has_lt α]
[contravariant_class α α (function.swap has_add.add) has_lt.lt]
{a b : α}
(h : b < a + b) :
0 < a
theorem
neg_of_add_lt_left
{α : Type u_1}
[add_zero_class α]
[has_lt α]
[contravariant_class α α (function.swap has_add.add) has_lt.lt]
{a b : α}
(h : a + b < b) :
a < 0
theorem
lt_one_of_mul_lt_left
{α : Type u_1}
[mul_one_class α]
[has_lt α]
[contravariant_class α α (function.swap has_mul.mul) has_lt.lt]
{a b : α}
(h : a * b < b) :
a < 1
@[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
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_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
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 : α) :
Lemmas of the form b ≤ c → a ≤ 1 → b * a ≤ c,
which assume left covariance.
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
add_lt_of_le_of_neg
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_lt.lt]
{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]
{a b c : α}
(hbc : b ≤ c)
(ha : a < 1) :
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
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 : α}
(hbc : b < c)
(ha : a < 1) :
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 : α}
(hbc : b < c)
(ha : a < 0) :
theorem
mul_lt_of_lt_of_lt_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_lt_of_lt_of_neg'
{α : 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
left.add_nonpos
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
{a b : α}
(ha : a ≤ 0)
(hb : b ≤ 0) :
Assumes left covariance.
The lemma assuming right covariance is right.add_nonpos.
theorem
left.mul_le_one
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{a b : α}
(ha : a ≤ 1)
(hb : b ≤ 1) :
Assumes left covariance.
The lemma assuming right covariance is right.mul_le_one.
theorem
left.mul_lt_one_of_le_of_lt
{α : 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_of_le_of_lt.
theorem
left.add_neg_of_nonpos_of_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_of_nonpos_of_neg.
theorem
left.mul_lt_one_of_lt_of_le
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{a b : α}
(ha : a < 1)
(hb : b ≤ 1) :
Assumes left covariance.
The lemma assuming right covariance is right.mul_lt_one_of_lt_of_le.
theorem
left.add_neg_of_neg_of_nonpos
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
{a b : α}
(ha : a < 0)
(hb : b ≤ 0) :
Assumes left covariance.
The lemma assuming right covariance is right.add_neg_of_neg_of_nonpos.
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
left.mul_lt_one'
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{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_le.le]
{a b : α}
(ha : a < 0)
(hb : b < 0) :
Assumes left covariance.
The lemma assuming right covariance is right.add_neg'.
Lemmas of the form b ≤ c → 1 ≤ a → b ≤ c * a,
which assume left covariance.
theorem
le_add_of_le_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
le_mul_of_le_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_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
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
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 : α}
(hbc : b < c)
(ha : 1 < a) :
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 : α}
(hbc : b < c)
(ha : 0 < a) :
theorem
lt_add_of_lt_of_pos'
{α : 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
lt_mul_of_lt_of_one_lt'
{α : 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
left.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) :
Assumes left covariance.
The lemma assuming right covariance is right.one_le_mul.
theorem
left.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) :
Assumes left covariance.
The lemma assuming right covariance is right.add_nonneg.
theorem
left.add_pos_of_nonneg_of_pos
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_lt.lt]
{a b : α}
(ha : 0 ≤ a)
(hb : 0 < b) :
Assumes left covariance.
The lemma assuming right covariance is right.add_pos_of_nonneg_of_pos.
theorem
left.one_lt_mul_of_le_of_lt
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_lt.lt]
{a b : α}
(ha : 1 ≤ a)
(hb : 1 < b) :
Assumes left covariance.
The lemma assuming right covariance is right.one_lt_mul_of_le_of_lt.
theorem
left.add_pos_of_pos_of_nonneg
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
{a b : α}
(ha : 0 < a)
(hb : 0 ≤ b) :
Assumes left covariance.
The lemma assuming right covariance is right.add_pos_of_pos_of_nonneg.
theorem
left.one_lt_mul_of_lt_of_le
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{a b : α}
(ha : 1 < a)
(hb : 1 ≤ b) :
Assumes left covariance.
The lemma assuming right covariance is right.one_lt_mul_of_lt_of_le.
theorem
left.one_lt_mul
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_lt.lt]
{a b : α}
(ha : 1 < a)
(hb : 1 < b) :
Assumes left covariance.
The lemma assuming right covariance is right.one_lt_mul.
theorem
left.add_pos
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_lt.lt]
{a b : α}
(ha : 0 < a)
(hb : 0 < b) :
Assumes left covariance.
The lemma assuming right covariance is right.add_pos.
theorem
left.add_pos'
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
{a b : α}
(ha : 0 < a)
(hb : 0 < b) :
Assumes left covariance.
The lemma assuming right covariance is right.add_pos'.
theorem
left.one_lt_mul'
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{a b : α}
(ha : 1 < a)
(hb : 1 < b) :
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.
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
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
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_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) :
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) :
theorem
mul_lt_of_lt_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)
(hbc : b < c) :
theorem
add_lt_of_neg_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)
(hbc : b < c) :
theorem
right.mul_le_one
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b : α}
(ha : a ≤ 1)
(hb : b ≤ 1) :
Assumes right covariance.
The lemma assuming left covariance is left.mul_le_one.
theorem
right.add_nonpos
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b : α}
(ha : a ≤ 0)
(hb : b ≤ 0) :
Assumes right covariance.
The lemma assuming left covariance is left.add_nonpos.
theorem
right.add_neg_of_neg_of_nonpos
{α : 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_of_neg_of_nonpos.
theorem
right.mul_lt_one_of_lt_of_le
{α : 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_of_lt_of_le.
theorem
right.mul_lt_one_of_le_of_lt
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b : α}
(ha : a ≤ 1)
(hb : b < 1) :
Assumes right covariance.
The lemma assuming left covariance is left.mul_lt_one_of_le_of_lt.
theorem
right.add_neg_of_nonpos_of_neg
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b : α}
(ha : a ≤ 0)
(hb : b < 0) :
Assumes right covariance.
The lemma assuming left covariance is left.add_neg_of_nonpos_of_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
right.add_neg'
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{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_le.le]
{a b : α}
(ha : a < 1)
(hb : b < 1) :
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.
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
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
lt_mul_of_one_le_of_lt
{α : 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
lt_add_of_nonneg_of_lt
{α : 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
lt_mul_of_one_lt_of_lt
{α : 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
lt_add_of_pos_of_lt
{α : 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_add_of_pos_of_lt'
{α : 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
lt_mul_of_one_lt_of_lt'
{α : 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
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.
The lemma assuming left covariance is left.add_nonneg.
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.
The lemma assuming left covariance is left.one_le_mul.
theorem
right.add_pos_of_pos_of_nonneg
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
{a b : α}
(ha : 0 < a)
(hb : 0 ≤ b) :
Assumes right covariance.
The lemma assuming left covariance is left.add_pos_of_pos_of_nonneg.
theorem
right.one_lt_mul_of_lt_of_le
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
{a b : α}
(ha : 1 < a)
(hb : 1 ≤ b) :
Assumes right covariance.
The lemma assuming left covariance is left.one_lt_mul_of_lt_of_le.
theorem
right.add_pos_of_nonneg_of_pos
{α : 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.
The lemma assuming left covariance is left.add_pos_of_nonneg_of_pos.
theorem
right.one_lt_mul_of_le_of_lt
{α : 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.
The lemma assuming left covariance is left.one_lt_mul_of_le_of_lt.
theorem
right.add_pos
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
{a b : α}
(ha : 0 < a)
(hb : 0 < b) :
Assumes right covariance.
The lemma assuming left covariance is left.add_pos.
theorem
right.one_lt_mul
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
{a b : α}
(ha : 1 < a)
(hb : 1 < b) :
Assumes right covariance.
The lemma assuming left covariance is left.one_lt_mul.
theorem
right.add_pos'
{α : 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.
The lemma assuming left covariance is left.add_pos'.
theorem
right.one_lt_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.
The lemma assuming left covariance is left.one_lt_mul'.
theorem
mul_le_one'
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{a b : α}
(ha : a ≤ 1)
(hb : b ≤ 1) :
Alias of left.mul_le_one.
theorem
mul_lt_one_of_le_of_lt
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_lt.lt]
{a b : α}
(ha : a ≤ 1)
(hb : b < 1) :
Alias of left.mul_lt_one_of_le_of_lt.
theorem
mul_lt_one_of_lt_of_le
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{a b : α}
(ha : a < 1)
(hb : b ≤ 1) :
Alias of left.mul_lt_one_of_lt_of_le.
theorem
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) :
Alias of left.mul_lt_one.
theorem
mul_lt_one'
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{a b : α}
(ha : a < 1)
(hb : b < 1) :
Alias of left.mul_lt_one'.
theorem
add_nonpos
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
{a b : α}
(ha : a ≤ 0)
(hb : b ≤ 0) :
Alias of left.add_nonpos.
theorem
add_neg_of_nonpos_of_neg
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_lt.lt]
{a b : α}
(ha : a ≤ 0)
(hb : b < 0) :
Alias of left.add_neg_of_nonpos_of_neg.
theorem
add_neg_of_neg_of_nonpos
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
{a b : α}
(ha : a < 0)
(hb : b ≤ 0) :
Alias of left.add_neg_of_neg_of_nonpos.
theorem
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) :
Alias of left.add_neg.
theorem
add_neg'
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
{a b : α}
(ha : a < 0)
(hb : b < 0) :
Alias of left.add_neg'.
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) :
Alias of left.one_le_mul.
theorem
one_lt_mul_of_le_of_lt'
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_lt.lt]
{a b : α}
(ha : 1 ≤ a)
(hb : 1 < b) :
Alias of left.one_lt_mul_of_le_of_lt.
theorem
one_lt_mul_of_lt_of_le'
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{a b : α}
(ha : 1 < a)
(hb : 1 ≤ b) :
Alias of left.one_lt_mul_of_lt_of_le.
theorem
one_lt_mul'
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_lt.lt]
{a b : α}
(ha : 1 < a)
(hb : 1 < b) :
Alias of left.one_lt_mul.
theorem
one_lt_mul''
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{a b : α}
(ha : 1 < a)
(hb : 1 < b) :
Alias of left.one_lt_mul'.
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) :
Alias of left.add_nonneg.
theorem
add_pos_of_nonneg_of_pos
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_lt.lt]
{a b : α}
(ha : 0 ≤ a)
(hb : 0 < b) :
Alias of left.add_pos_of_nonneg_of_pos.
theorem
add_pos_of_pos_of_nonneg
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
{a b : α}
(ha : 0 < a)
(hb : 0 ≤ b) :
Alias of left.add_pos_of_pos_of_nonneg.
theorem
add_pos
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_lt.lt]
{a b : α}
(ha : 0 < a)
(hb : 0 < b) :
Alias of left.add_pos.
theorem
add_pos'
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
{a b : α}
(ha : 0 < a)
(hb : 0 < b) :
Alias of left.add_pos'.
theorem
lt_of_mul_lt_of_one_le_left
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{a b c : α}
(h : a * b < c)
(hle : 1 ≤ b) :
a < c
theorem
lt_of_add_lt_of_nonneg_left
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
{a b c : α}
(h : a + b < c)
(hle : 0 ≤ b) :
a < c
theorem
le_of_mul_le_of_one_le_left
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{a b c : α}
(h : a * b ≤ c)
(hle : 1 ≤ b) :
a ≤ c
theorem
le_of_add_le_of_nonneg_left
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
{a b c : α}
(h : a + b ≤ c)
(hle : 0 ≤ b) :
a ≤ c
theorem
lt_of_lt_add_of_nonpos_left
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
{a b c : α}
(h : a < b + c)
(hle : c ≤ 0) :
a < b
theorem
lt_of_lt_mul_of_le_one_left
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{a b c : α}
(h : a < b * c)
(hle : c ≤ 1) :
a < b
theorem
le_of_le_add_of_nonpos_left
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
{a b c : α}
(h : a ≤ b + c)
(hle : c ≤ 0) :
a ≤ b
theorem
le_of_le_mul_of_le_one_left
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
{a b c : α}
(h : a ≤ b * c)
(hle : c ≤ 1) :
a ≤ b
theorem
lt_of_mul_lt_of_one_le_right
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b c : α}
(h : a * b < c)
(hle : 1 ≤ a) :
b < c
theorem
lt_of_add_lt_of_nonneg_right
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b c : α}
(h : a + b < c)
(hle : 0 ≤ a) :
b < c
theorem
le_of_mul_le_of_one_le_right
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b c : α}
(h : a * b ≤ c)
(hle : 1 ≤ a) :
b ≤ c
theorem
le_of_add_le_of_nonneg_right
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b c : α}
(h : a + b ≤ c)
(hle : 0 ≤ a) :
b ≤ c
theorem
lt_of_lt_add_of_nonpos_right
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b c : α}
(h : a < b + c)
(hle : b ≤ 0) :
a < c
theorem
lt_of_lt_mul_of_le_one_right
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b c : α}
(h : a < b * c)
(hle : b ≤ 1) :
a < c
theorem
le_of_le_mul_of_le_one_right
{α : Type u_1}
[mul_one_class α]
[preorder α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b c : α}
(h : a ≤ b * c)
(hle : b ≤ 1) :
a ≤ c
theorem
le_of_le_add_of_nonpos_right
{α : Type u_1}
[add_zero_class α]
[preorder α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b c : α}
(h : a ≤ b + c)
(hle : b ≤ 0) :
a ≤ c
theorem
add_eq_zero_iff'
{α : Type u_1}
[add_zero_class α]
[partial_order α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b : α}
(ha : 0 ≤ a)
(hb : 0 ≤ b) :
theorem
mul_eq_one_iff'
{α : Type u_1}
[mul_one_class α]
[partial_order α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b : α}
(ha : 1 ≤ a)
(hb : 1 ≤ b) :
theorem
mul_le_mul_iff_of_ge
{α : Type u_1}
[mul_one_class α]
[partial_order α]
[covariant_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]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
{a₁ a₂ b₁ b₂ : α}
(ha : a₁ ≤ a₂)
(hb : b₁ ≤ b₂) :
theorem
add_le_add_iff_of_ge
{α : Type u_1}
[add_zero_class α]
[partial_order α]
[covariant_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]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
{a₁ a₂ b₁ b₂ : α}
(ha : a₁ ≤ a₂)
(hb : b₁ ≤ b₂) :
theorem
eq_zero_of_add_nonneg_left
{α : Type u_1}
[add_zero_class α]
[partial_order α]
[covariant_class α α has_add.add has_le.le]
{a b : α}
(ha : a ≤ 0)
(hb : b ≤ 0)
(hab : 0 ≤ a + b) :
a = 0
theorem
eq_one_of_one_le_mul_left
{α : Type u_1}
[mul_one_class α]
[partial_order α]
[covariant_class α α has_mul.mul has_le.le]
{a b : α}
(ha : a ≤ 1)
(hb : b ≤ 1)
(hab : 1 ≤ a * b) :
a = 1
theorem
eq_one_of_mul_le_one_left
{α : Type u_1}
[mul_one_class α]
[partial_order α]
[covariant_class α α has_mul.mul has_le.le]
{a b : α}
(ha : 1 ≤ a)
(hb : 1 ≤ b)
(hab : a * b ≤ 1) :
a = 1
theorem
eq_zero_of_add_nonpos_left
{α : Type u_1}
[add_zero_class α]
[partial_order α]
[covariant_class α α has_add.add has_le.le]
{a b : α}
(ha : 0 ≤ a)
(hb : 0 ≤ b)
(hab : a + b ≤ 0) :
a = 0
theorem
eq_one_of_one_le_mul_right
{α : Type u_1}
[mul_one_class α]
[partial_order α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b : α}
(ha : a ≤ 1)
(hb : b ≤ 1)
(hab : 1 ≤ a * b) :
b = 1
theorem
eq_zero_of_add_nonneg_right
{α : Type u_1}
[add_zero_class α]
[partial_order α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b : α}
(ha : a ≤ 0)
(hb : b ≤ 0)
(hab : 0 ≤ a + b) :
b = 0
theorem
eq_one_of_mul_le_one_right
{α : Type u_1}
[mul_one_class α]
[partial_order α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b : α}
(ha : 1 ≤ a)
(hb : 1 ≤ b)
(hab : a * b ≤ 1) :
b = 1
theorem
eq_zero_of_add_nonpos_right
{α : Type u_1}
[add_zero_class α]
[partial_order α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b : α}
(ha : 0 ≤ a)
(hb : 0 ≤ b)
(hab : a + b ≤ 0) :
b = 0
theorem
exists_square_le
{α : Type u_1}
[mul_one_class α]
[linear_order α]
[covariant_class α α has_mul.mul has_lt.lt]
(a : α) :
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
left.mul_eq_mul_iff_eq_and_eq
{α : Type u_1}
[semigroup α]
[partial_order α]
[covariant_class α α has_mul.mul has_lt.lt]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
[contravariant_class α α has_mul.mul has_le.le]
[contravariant_class α α (function.swap has_mul.mul) has_le.le]
{a b c d : α}
(hac : a ≤ c)
(hbd : b ≤ d) :
theorem
left.add_eq_add_iff_eq_and_eq
{α : Type u_1}
[add_semigroup α]
[partial_order α]
[covariant_class α α has_add.add has_lt.lt]
[covariant_class α α (function.swap has_add.add) has_le.le]
[contravariant_class α α has_add.add has_le.le]
[contravariant_class α α (function.swap has_add.add) has_le.le]
{a b c d : α}
(hac : a ≤ c)
(hbd : b ≤ d) :
theorem
right.add_eq_add_iff_eq_and_eq
{α : Type u_1}
[add_semigroup α]
[partial_order α]
[covariant_class α α has_add.add has_le.le]
[contravariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap 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
right.mul_eq_mul_iff_eq_and_eq
{α : Type u_1}
[semigroup α]
[partial_order α]
[covariant_class α α has_mul.mul has_le.le]
[contravariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap 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_eq_mul_iff_eq_and_eq
{α : Type u_1}
[semigroup α]
[partial_order α]
[covariant_class α α has_mul.mul has_lt.lt]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
[contravariant_class α α has_mul.mul has_le.le]
[contravariant_class α α (function.swap has_mul.mul) has_le.le]
{a b c d : α}
(hac : a ≤ c)
(hbd : b ≤ d) :
Alias of left.mul_eq_mul_iff_eq_and_eq.
theorem
add_eq_add_iff_eq_and_eq
{α : Type u_1}
[add_semigroup α]
[partial_order α]
[covariant_class α α has_add.add has_lt.lt]
[covariant_class α α (function.swap has_add.add) has_le.le]
[contravariant_class α α has_add.add has_le.le]
[contravariant_class α α (function.swap has_add.add) has_le.le]
{a b c d : α}
(hac : a ≤ c)
(hbd : b ≤ d) :
Alias of left.mul_eq_mul_iff_eq_and_eq.
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_on.const_add
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f : β → α}
{s : set β}
[covariant_class α α has_add.add has_le.le]
(hf : monotone_on f s)
(a : α) :
monotone_on (λ (x : β), a + f x) s
theorem
monotone_on.const_mul'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f : β → α}
{s : set β}
[covariant_class α α has_mul.mul has_le.le]
(hf : monotone_on f s)
(a : α) :
monotone_on (λ (x : β), a * f x) s
theorem
antitone.const_add
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f : β → α}
[covariant_class α α has_add.add has_le.le]
(hf : antitone f)
(a : α) :
theorem
antitone.const_mul'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f : β → α}
[covariant_class α α has_mul.mul has_le.le]
(hf : antitone f)
(a : α) :
theorem
antitone_on.const_mul'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f : β → α}
{s : set β}
[covariant_class α α has_mul.mul has_le.le]
(hf : antitone_on f s)
(a : α) :
antitone_on (λ (x : β), a * f x) s
theorem
antitone_on.const_add
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f : β → α}
{s : set β}
[covariant_class α α has_add.add has_le.le]
(hf : antitone_on f s)
(a : α) :
antitone_on (λ (x : β), a + f x) s
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_on.mul_const'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f : β → α}
{s : set β}
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(hf : monotone_on f s)
(a : α) :
monotone_on (λ (x : β), f x * a) s
theorem
monotone_on.add_const
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f : β → α}
{s : set β}
[covariant_class α α (function.swap has_add.add) has_le.le]
(hf : monotone_on f s)
(a : α) :
monotone_on (λ (x : β), f x + a) s
theorem
antitone.mul_const'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f : β → α}
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(hf : antitone f)
(a : α) :
theorem
antitone.add_const
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f : β → α}
[covariant_class α α (function.swap has_add.add) has_le.le]
(hf : antitone f)
(a : α) :
theorem
antitone_on.mul_const'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f : β → α}
{s : set β}
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(hf : antitone_on f s)
(a : α) :
antitone_on (λ (x : β), f x * a) s
theorem
antitone_on.add_const
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f : β → α}
{s : set β}
[covariant_class α α (function.swap has_add.add) has_le.le]
(hf : antitone_on f s)
(a : α) :
antitone_on (λ (x : β), f x + a) s
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
monotone_on.mul'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f g : β → α}
{s : set β}
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(hf : monotone_on f s)
(hg : monotone_on g s) :
monotone_on (λ (x : β), f x * g x) s
The product of two monotone functions is monotone.
theorem
monotone_on.add
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f g : β → α}
{s : set β}
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(hf : monotone_on f s)
(hg : monotone_on g s) :
monotone_on (λ (x : β), f x + g x) s
The sum of two monotone functions is monotone.
theorem
antitone.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 : antitone f)
(hg : antitone g) :
The sum of two antitone functions is antitone.
theorem
antitone.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 : antitone f)
(hg : antitone g) :
The product of two antitone functions is antitone.
theorem
antitone_on.mul'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f g : β → α}
{s : set β}
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(hf : antitone_on f s)
(hg : antitone_on g s) :
antitone_on (λ (x : β), f x * g x) s
The product of two antitone functions is antitone.
theorem
antitone_on.add
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f g : β → α}
{s : set β}
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(hf : antitone_on f s)
(hg : antitone_on g s) :
antitone_on (λ (x : β), f x + g x) s
The sum of two antitone functions is antitone.
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_on.const_mul'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f : β → α}
{s : set β}
[covariant_class α α has_mul.mul has_lt.lt]
(hf : strict_mono_on f s)
(c : α) :
strict_mono_on (λ (x : β), c * f x) s
theorem
strict_mono_on.const_add
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f : β → α}
{s : set β}
[covariant_class α α has_add.add has_lt.lt]
(hf : strict_mono_on f s)
(c : α) :
strict_mono_on (λ (x : β), c + f x) s
theorem
strict_anti.const_add
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f : β → α}
[covariant_class α α has_add.add has_lt.lt]
(hf : strict_anti f)
(c : α) :
strict_anti (λ (x : β), c + f x)
theorem
strict_anti.const_mul'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f : β → α}
[covariant_class α α has_mul.mul has_lt.lt]
(hf : strict_anti f)
(c : α) :
strict_anti (λ (x : β), c * f x)
theorem
strict_anti_on.const_add
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f : β → α}
{s : set β}
[covariant_class α α has_add.add has_lt.lt]
(hf : strict_anti_on f s)
(c : α) :
strict_anti_on (λ (x : β), c + f x) s
theorem
strict_anti_on.const_mul'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f : β → α}
{s : set β}
[covariant_class α α has_mul.mul has_lt.lt]
(hf : strict_anti_on f s)
(c : α) :
strict_anti_on (λ (x : β), c * f x) s
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_on.add_const
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f : β → α}
{s : set β}
[covariant_class α α (function.swap has_add.add) has_lt.lt]
(hf : strict_mono_on f s)
(c : α) :
strict_mono_on (λ (x : β), f x + c) s
theorem
strict_mono_on.mul_const'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f : β → α}
{s : set β}
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
(hf : strict_mono_on f s)
(c : α) :
strict_mono_on (λ (x : β), f x * c) s
theorem
strict_anti.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_anti f)
(c : α) :
strict_anti (λ (x : β), f x * c)
theorem
strict_anti.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_anti f)
(c : α) :
strict_anti (λ (x : β), f x + c)
theorem
strict_anti_on.add_const
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f : β → α}
{s : set β}
[covariant_class α α (function.swap has_add.add) has_lt.lt]
(hf : strict_anti_on f s)
(c : α) :
strict_anti_on (λ (x : β), f x + c) s
theorem
strict_anti_on.mul_const'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f : β → α}
{s : set β}
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
(hf : strict_anti_on f s)
(c : α) :
strict_anti_on (λ (x : β), f x * c) s
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
strict_mono_on.mul'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f g : β → α}
{s : set β}
[covariant_class α α has_mul.mul has_lt.lt]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
(hf : strict_mono_on f s)
(hg : strict_mono_on g s) :
strict_mono_on (λ (x : β), f x * g x) s
The product of two strictly monotone functions is strictly monotone.
theorem
strict_mono_on.add
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f g : β → α}
{s : set β}
[covariant_class α α has_add.add has_lt.lt]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
(hf : strict_mono_on f s)
(hg : strict_mono_on g s) :
strict_mono_on (λ (x : β), f x + g x) s
The sum of two strictly monotone functions is strictly monotone.
theorem
strict_anti.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_anti f)
(hg : strict_anti g) :
strict_anti (λ (x : β), f x + g x)
The sum of two strictly antitone functions is strictly antitone.
theorem
strict_anti.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_anti f)
(hg : strict_anti g) :
strict_anti (λ (x : β), f x * g x)
The product of two strictly antitone functions is strictly antitone.
theorem
strict_anti_on.mul'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f g : β → α}
{s : set β}
[covariant_class α α has_mul.mul has_lt.lt]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
(hf : strict_anti_on f s)
(hg : strict_anti_on g s) :
strict_anti_on (λ (x : β), f x * g x) s
The product of two strictly antitone functions is strictly antitone.
theorem
strict_anti_on.add
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f g : β → α}
{s : set β}
[covariant_class α α has_add.add has_lt.lt]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
(hf : strict_anti_on f s)
(hg : strict_anti_on g s) :
strict_anti_on (λ (x : β), f x + g x) s
The sum of two strictly antitone functions is strictly antitone.
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
monotone_on.add_strict_mono
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{s : set β}
[covariant_class α α has_add.add has_lt.lt]
[covariant_class α α (function.swap has_add.add) has_le.le]
{f g : β → α}
(hf : monotone_on f s)
(hg : strict_mono_on g s) :
strict_mono_on (λ (x : β), f x + g x) s
The sum of a monotone function and a strictly monotone function is strictly monotone.
theorem
monotone_on.mul_strict_mono'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{s : set β}
[covariant_class α α has_mul.mul has_lt.lt]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{f g : β → α}
(hf : monotone_on f s)
(hg : strict_mono_on g s) :
strict_mono_on (λ (x : β), f x * g x) s
The product of a monotone function and a strictly monotone function is strictly monotone.
theorem
antitone.mul_strict_anti'
{α : 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 : antitone f)
(hg : strict_anti g) :
strict_anti (λ (x : β), f x * g x)
The product of a antitone function and a strictly antitone function is strictly antitone.
theorem
antitone.add_strict_anti
{α : 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 : antitone f)
(hg : strict_anti g) :
strict_anti (λ (x : β), f x + g x)
The sum of a antitone function and a strictly antitone function is strictly antitone.
theorem
antitone_on.mul_strict_anti'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{s : set β}
[covariant_class α α has_mul.mul has_lt.lt]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{f g : β → α}
(hf : antitone_on f s)
(hg : strict_anti_on g s) :
strict_anti_on (λ (x : β), f x * g x) s
The product of a antitone function and a strictly antitone function is strictly antitone.
theorem
antitone_on.add_strict_anti
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{s : set β}
[covariant_class α α has_add.add has_lt.lt]
[covariant_class α α (function.swap has_add.add) has_le.le]
{f g : β → α}
(hf : antitone_on f s)
(hg : strict_anti_on g s) :
strict_anti_on (λ (x : β), f x + g x) s
The sum of a antitone function and a strictly antitone function is strictly antitone.
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.
theorem
strict_mono_on.add_monotone
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f g : β → α}
{s : set β}
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
(hf : strict_mono_on f s)
(hg : monotone_on g s) :
strict_mono_on (λ (x : β), f x + g x) s
The sum of a strictly monotone function and a monotone function is strictly monotone.
theorem
strict_mono_on.mul_monotone'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f g : β → α}
{s : set β}
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
(hf : strict_mono_on f s)
(hg : monotone_on g s) :
strict_mono_on (λ (x : β), f x * g x) s
The product of a strictly monotone function and a monotone function is strictly monotone.
theorem
strict_anti.mul_antitone'
{α : 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_anti f)
(hg : antitone g) :
strict_anti (λ (x : β), f x * g x)
The product of a strictly antitone function and a antitone function is strictly antitone.
theorem
strict_anti.add_antitone
{α : 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_anti f)
(hg : antitone g) :
strict_anti (λ (x : β), f x + g x)
The sum of a strictly antitone function and a antitone function is strictly antitone.
theorem
strict_anti_on.add_antitone
{α : Type u_1}
{β : Type u_2}
[has_add α]
[preorder α]
[preorder β]
{f g : β → α}
{s : set β}
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
(hf : strict_anti_on f s)
(hg : antitone_on g s) :
strict_anti_on (λ (x : β), f x + g x) s
The sum of a strictly antitone function and a antitone function is strictly antitone.
theorem
strict_anti_on.mul_antitone'
{α : Type u_1}
{β : Type u_2}
[has_mul α]
[preorder α]
[preorder β]
{f g : β → α}
{s : set β}
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
(hf : strict_anti_on f s)
(hg : antitone_on g s) :
strict_anti_on (λ (x : β), f x * g x) s
The product of a strictly antitone function and a antitone function is strictly antitone.
@[simp]
theorem
cmp_add_left
{α : Type u_1}
[has_add α]
[linear_order α]
[covariant_class α α has_add.add has_lt.lt]
(a b c : α) :
@[simp]
theorem
cmp_mul_left'
{α : Type u_1}
[has_mul α]
[linear_order α]
[covariant_class α α has_mul.mul has_lt.lt]
(a b c : α) :
@[simp]
theorem
cmp_mul_right'
{α : Type u_1}
[has_mul α]
[linear_order α]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
(a b c : α) :
@[simp]
theorem
cmp_add_right
{α : Type u_1}
[has_add α]
[linear_order α]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
(a b c : α) :
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) :
theorem
bit0_mono
{α : Type u_1}
[has_add α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le] :
theorem
bit0_strict_mono
{α : Type u_1}
[has_add α]
[preorder α]
[covariant_class α α has_add.add has_lt.lt]
[covariant_class α α (function.swap has_add.add) has_lt.lt] :