mathlib documentation

algebra.ordered_monoid_lemmas

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 #

No monoid is actually present in this file: all assumptions have been generalized to has_mul or mul_one_class.

theorem lt_of_add_lt_add_left {α : Type u_1} {a b c : α} [preorder α] [has_add α] [contravariant_class α α has_add.add has_lt.lt] :
a + b < a + cb < c
theorem lt_of_mul_lt_mul_left' {α : Type u_1} {a b c : α} [preorder α] [has_mul α] [contravariant_class α α has_mul.mul has_lt.lt] :
a * b < a * cb < c
theorem mul_le_mul_left' {α : Type u_1} {a b : α} [preorder α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] (h : a b) (c : α) :
c * a c * b
theorem add_le_add_left {α : Type u_1} {a b : α} [preorder α] [has_add α] [covariant_class α α has_add.add has_le.le] (h : a b) (c : α) :
c + a c + b
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) :
a * d < c
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) :
a + d < c
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) :
a + d c
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) :
a * d c
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) :
a < b + 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) :
a < b * 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) :
a b + 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) :
a b * d
theorem le_add_of_nonneg_right {α : Type u_1} {a b : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] (h : 0 b) :
a a + b
theorem le_mul_of_one_le_right' {α : Type u_1} {a b : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] (h : 1 b) :
a a * b
theorem mul_le_of_le_one_right' {α : Type u_1} {a b : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] (h : b 1) :
a * b a
theorem add_le_of_nonpos_right {α : Type u_1} {a b : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] (h : b 0) :
a + b a
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 lt_of_add_lt_add_right {α : Type u_1} {a b c : α} [preorder α] [has_add α] [contravariant_class α α (function.swap has_add.add) has_lt.lt] (h : a + b < c + b) :
a < c
theorem lt_of_mul_lt_mul_right' {α : Type u_1} {a b c : α} [preorder α] [has_mul α] [contravariant_class α α (function.swap has_mul.mul) has_lt.lt] (h : a * b < c * b) :
a < c
theorem add_le_add_right {α : Type u_1} {a b : α} [preorder α] [has_add α] [covariant_class α α (function.swap has_add.add) has_le.le] (h : a b) (c : α) :
a + c b + c
theorem mul_le_mul_right' {α : Type u_1} {a b : α} [preorder α] [has_mul α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (h : a b) (c : α) :
a * c b * c
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) :
d * b < c
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) :
d + b < c
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) :
d * b c
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) :
d + b c
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) :
a < d + c
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) :
a < d * c
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) :
a d * c
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) :
a d + c
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) :
a b * a
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) :
a b + a
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) :
b + a a
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) :
b * a a
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 add_le_add {α : 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_le.le] (h₁ : a b) (h₂ : c d) :
a + c b + d
theorem mul_le_mul' {α : 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_le.le] (h₁ : a b) (h₂ : c d) :
a * c b * d
theorem mul_le_mul_three {α : 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_le.le] {e f : α} (h₁ : a d) (h₂ : b e) (h₃ : c f) :
(a * b) * c (d * e) * f
theorem add_le_add_three {α : 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_le.le] {e f : α} (h₁ : a d) (h₂ : b e) (h₃ : c f) :
a + b + c d + e + f
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) :
1 < a * 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) :
0 < a + 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) :
1 < a * 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) :
0 < a + 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) :
b < c * 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) :
b < c + 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) :
b < c + 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) :
b < c * a
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) :
0 < a + 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) :
1 < a * 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) :
b < a * 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) :
b < a + 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) :
b < a + 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) :
b < a * c
theorem le_add_of_nonneg_of_le {α : Type u_1} {a b c : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (ha : 0 a) (hbc : b c) :
b a + c
theorem le_mul_of_one_le_of_le {α : Type u_1} {a b c : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (ha : 1 a) (hbc : b c) :
b a * c
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] [covariant_class α α (function.swap has_add.add) has_le.le] (hbc : b c) (ha : 0 a) :
b c + 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] [covariant_class α α (function.swap has_mul.mul) has_le.le] (hbc : b c) (ha : 1 a) :
b c * a
theorem one_le_mul {α : Type u_1} {a b : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (ha : 1 a) (hb : 1 b) :
1 a * b
theorem add_nonneg {α : Type u_1} {a b : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (ha : 0 a) (hb : 0 b) :
0 a + b
theorem add_nonpos {α : Type u_1} {a b : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (ha : a 0) (hb : b 0) :
a + b 0
theorem mul_le_one' {α : Type u_1} {a b : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (ha : a 1) (hb : b 1) :
a * b 1
theorem mul_le_of_le_one_of_le' {α : Type u_1} {a b c : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (ha : a 1) (hbc : b c) :
a * b c
theorem add_le_of_nonpos_of_le' {α : Type u_1} {a b c : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (ha : a 0) (hbc : b c) :
a + b c
theorem add_le_of_le_of_nonpos' {α : Type u_1} {a b c : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (hbc : b c) (ha : a 0) :
b + a c
theorem mul_le_of_le_of_le_one' {α : Type u_1} {a b c : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (hbc : b c) (ha : a 1) :
b * a c
theorem add_neg_of_neg_of_nonpos' {α : Type u_1} {a b : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (ha : a < 0) (hb : b 0) :
a + b < 0
theorem mul_lt_one_of_lt_one_of_le_one' {α : Type u_1} {a b : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (ha : a < 1) (hb : b 1) :
a * b < 1
theorem mul_lt_one_of_le_one_of_lt_one' {α : Type u_1} {a b : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (ha : a 1) (hb : b < 1) :
a * b < 1
theorem add_neg_of_nonpos_of_neg' {α : Type u_1} {a b : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (ha : a 0) (hb : b < 0) :
a + b < 0
theorem mul_lt_one' {α : Type u_1} {a b : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (ha : a < 1) (hb : b < 1) :
a * b < 1
theorem add_neg' {α : Type u_1} {a b : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (ha : a < 0) (hb : b < 0) :
a + b < 0
theorem add_lt_of_nonpos_of_lt' {α : Type u_1} {a b c : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (ha : a 0) (hbc : b < c) :
a + b < c
theorem mul_lt_of_le_one_of_lt' {α : Type u_1} {a b c : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (ha : a 1) (hbc : b < c) :
a * b < c
theorem mul_lt_of_lt_of_le_one' {α : Type u_1} {a b c : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (hbc : b < c) (ha : a 1) :
b * a < c
theorem add_lt_of_lt_of_nonpos' {α : Type u_1} {a b c : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (hbc : b < c) (ha : a 0) :
b + a < c
theorem mul_lt_of_lt_one_of_lt' {α : Type u_1} {a b c : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (ha : a < 1) (hbc : b < c) :
a * b < c
theorem add_lt_of_neg_of_lt' {α : Type u_1} {a b c : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (ha : a < 0) (hbc : b < c) :
a + b < c
theorem mul_lt_of_lt_of_lt_one' {α : Type u_1} {a b c : α} [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (hbc : b < c) (ha : a < 1) :
b * a < c
theorem add_lt_of_lt_of_neg' {α : Type u_1} {a b c : α} [preorder α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (hbc : b < c) (ha : a < 0) :
b + a < c
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) :
a + b = 0 a = 0 b = 0
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) :
a * b = 1 a = 1 b = 1
theorem le_of_mul_le_mul_left' {α : Type u_1} [partial_order α] [left_cancel_semigroup α] [contravariant_class α α has_mul.mul has_lt.lt] {a b c : α} (bc : a * b a * c) :
b c
theorem le_of_add_le_add_left {α : Type u_1} [partial_order α] [add_left_cancel_semigroup α] [contravariant_class α α has_add.add has_lt.lt] {a b c : α} (bc : a + b a + c) :
b c
theorem le_of_mul_le_mul_right' {α : Type u_1} [partial_order α] [right_cancel_semigroup α] [contravariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c : α} (bc : b * a c * a) :
b c
theorem le_of_add_le_add_right {α : Type u_1} [partial_order α] [add_right_cancel_semigroup α] [contravariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} (bc : b + a c + a) :
b c
theorem add_lt_add_left {α : Type u_1} {a b : α} [partial_order α] [add_left_cancel_monoid α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_lt.lt] (h : a < b) (c : α) :
c + a < c + b
theorem mul_lt_mul_left' {α : Type u_1} {a b : α} [partial_order α] [left_cancel_monoid α] [covariant_class α α has_mul.mul has_le.le] [contravariant_class α α has_mul.mul has_lt.lt] (h : a < b) (c : α) :
c * a < c * b
theorem lt_add_of_pos_right {α : Type u_1} [partial_order α] [add_left_cancel_monoid α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_lt.lt] (a : α) {b : α} (h : 0 < b) :
a < a + b
theorem lt_mul_of_one_lt_right' {α : Type u_1} [partial_order α] [left_cancel_monoid α] [covariant_class α α has_mul.mul has_le.le] [contravariant_class α α has_mul.mul has_lt.lt] (a : α) {b : α} (h : 1 < b) :
a < a * b
@[simp]
theorem mul_le_mul_iff_left {α : Type u_1} [partial_order α] [left_cancel_monoid α] [covariant_class α α has_mul.mul has_le.le] [contravariant_class α α has_mul.mul has_lt.lt] (a : α) {b c : α} :
a * b a * c b c
@[simp]
theorem add_le_add_iff_left {α : Type u_1} [partial_order α] [add_left_cancel_monoid α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_lt.lt] (a : α) {b c : α} :
a + b a + c b c
@[simp]
theorem mul_lt_mul_iff_left {α : Type u_1} [partial_order α] [left_cancel_monoid α] [covariant_class α α has_mul.mul has_le.le] [contravariant_class α α has_mul.mul has_lt.lt] (a : α) {b c : α} :
a * b < a * c b < c
@[simp]
theorem add_lt_add_iff_left {α : Type u_1} [partial_order α] [add_left_cancel_monoid α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_lt.lt] (a : α) {b c : α} :
a + b < a + c b < c
@[simp]
theorem le_add_iff_nonneg_right {α : Type u_1} [partial_order α] [add_left_cancel_monoid α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_lt.lt] (a : α) {b : α} :
a a + b 0 b
@[simp]
theorem le_mul_iff_one_le_right' {α : Type u_1} [partial_order α] [left_cancel_monoid α] [covariant_class α α has_mul.mul has_le.le] [contravariant_class α α has_mul.mul has_lt.lt] (a : α) {b : α} :
a a * b 1 b
@[simp]
theorem lt_add_iff_pos_right {α : Type u_1} [partial_order α] [add_left_cancel_monoid α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_lt.lt] (a : α) {b : α} :
a < a + b 0 < b
@[simp]
theorem lt_mul_iff_one_lt_right' {α : Type u_1} [partial_order α] [left_cancel_monoid α] [covariant_class α α has_mul.mul has_le.le] [contravariant_class α α has_mul.mul has_lt.lt] (a : α) {b : α} :
a < a * b 1 < b
@[simp]
@[simp]
@[simp]
theorem mul_lt_mul_right' {α : Type u_1} {a b : α} [partial_order α] [right_cancel_monoid α] [covariant_class α α (function.swap has_mul.mul) has_le.le] [contravariant_class α α (function.swap has_mul.mul) has_lt.lt] (h : a < b) (c : α) :
a * c < b * c
theorem add_lt_add_right {α : Type u_1} {a b : α} [partial_order α] [add_right_cancel_monoid α] [covariant_class α α (function.swap has_add.add) has_le.le] [contravariant_class α α (function.swap has_add.add) has_lt.lt] (h : a < b) (c : α) :
a + c < b + c
@[simp]
@[simp]
theorem mul_lt_mul_iff_right {α : Type u_1} {a b : α} [partial_order α] [right_cancel_monoid α] [covariant_class α α (function.swap has_mul.mul) has_le.le] [contravariant_class α α (function.swap has_mul.mul) has_lt.lt] (c : α) :
a * c < b * c a < b
@[simp]
theorem add_lt_add_of_lt_of_le {α : Type u_1} {a b c d : α} [partial_order α] [add_right_cancel_monoid α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (h₁ : a < b) (h₂ : c d) :
a + c < b + d
theorem mul_lt_mul_of_lt_of_le {α : Type u_1} {a b c d : α} [partial_order α] [right_cancel_monoid α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (h₁ : a < b) (h₂ : c d) :
a * c < b * d
theorem add_neg_of_neg_of_nonpos {α : Type u_1} {a b : α} [partial_order α] [add_right_cancel_monoid α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (ha : a < 0) (hb : b 0) :
a + b < 0
theorem mul_lt_one_of_lt_one_of_le_one {α : Type u_1} {a b : α} [partial_order α] [right_cancel_monoid α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (ha : a < 1) (hb : b 1) :
a * b < 1
theorem lt_add_of_pos_of_le {α : Type u_1} {a b c : α} [partial_order α] [add_right_cancel_monoid α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (ha : 0 < a) (hbc : b c) :
b < a + c
theorem lt_mul_of_one_lt_of_le {α : Type u_1} {a b c : α} [partial_order α] [right_cancel_monoid α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (ha : 1 < a) (hbc : b c) :
b < a * c
theorem add_le_of_nonpos_of_le {α : Type u_1} {a b c : α} [partial_order α] [add_right_cancel_monoid α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (ha : a 0) (hbc : b c) :
a + b c
theorem mul_le_of_le_one_of_le {α : Type u_1} {a b c : α} [partial_order α] [right_cancel_monoid α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (ha : a 1) (hbc : b c) :
a * b c
theorem mul_le_of_le_of_le_one {α : Type u_1} {a b c : α} [partial_order α] [right_cancel_monoid α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (hbc : b c) (ha : a 1) :
b * a c
theorem add_le_of_le_of_nonpos {α : Type u_1} {a b c : α} [partial_order α] [add_right_cancel_monoid α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (hbc : b c) (ha : a 0) :
b + a c
theorem mul_lt_of_lt_one_of_le {α : Type u_1} {a b c : α} [partial_order α] [right_cancel_monoid α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (ha : a < 1) (hbc : b c) :
a * b < c
theorem add_lt_of_neg_of_le {α : Type u_1} {a b c : α} [partial_order α] [add_right_cancel_monoid α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (ha : a < 0) (hbc : b c) :
a + b < c
theorem lt_mul_of_lt_of_one_le {α : Type u_1} {a b c : α} [partial_order α] [right_cancel_monoid α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (hbc : b < c) (ha : 1 a) :
b < c * a
theorem lt_add_of_lt_of_nonneg {α : Type u_1} {a b c : α} [partial_order α] [add_right_cancel_monoid α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (hbc : b < c) (ha : 0 a) :
b < c + a
theorem add_lt_of_lt_of_nonpos {α : Type u_1} {a b c : α} [partial_order α] [add_right_cancel_monoid α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (hbc : b < c) (ha : a 0) :
b + a < c
theorem mul_lt_of_lt_of_le_one {α : Type u_1} {a b c : α} [partial_order α] [right_cancel_monoid α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (hbc : b < c) (ha : a 1) :
b * a < c
theorem mul_lt_mul_of_le_of_lt {α : Type u_1} {a b c d : α} [partial_order α] [cancel_monoid α] [covariant_class α α has_mul.mul has_le.le] [contravariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_le.le] (h₁ : a b) (h₂ : c < d) :
a * c < b * d
theorem add_lt_add_of_le_of_lt {α : Type u_1} {a b c d : α} [partial_order α] [add_cancel_monoid α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_le.le] (h₁ : a b) (h₂ : c < d) :
a + c < b + d
theorem lt_add_of_le_of_pos {α : Type u_1} {a b c : α} [partial_order α] [add_cancel_monoid α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_le.le] (hbc : b c) (ha : 0 < a) :
b < c + a
theorem lt_mul_of_le_of_one_lt {α : Type u_1} {a b c : α} [partial_order α] [cancel_monoid α] [covariant_class α α has_mul.mul has_le.le] [contravariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_le.le] (hbc : b c) (ha : 1 < a) :
b < c * a
theorem add_lt_of_le_of_neg {α : Type u_1} {a b c : α} [partial_order α] [add_cancel_monoid α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_le.le] (hbc : b c) (ha : a < 0) :
b + a < c
theorem mul_lt_of_le_of_lt_one {α : Type u_1} {a b c : α} [partial_order α] [cancel_monoid α] [covariant_class α α has_mul.mul has_le.le] [contravariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_le.le] (hbc : b c) (ha : a < 1) :
b * a < c
theorem lt_mul_of_one_le_of_lt {α : Type u_1} {a b c : α} [partial_order α] [cancel_monoid α] [covariant_class α α has_mul.mul has_le.le] [contravariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_le.le] (ha : 1 a) (hbc : b < c) :
b < a * c
theorem lt_add_of_nonneg_of_lt {α : Type u_1} {a b c : α} [partial_order α] [add_cancel_monoid α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_le.le] (ha : 0 a) (hbc : b < c) :
b < a + c
theorem mul_lt_of_le_one_of_lt {α : Type u_1} {a b c : α} [partial_order α] [cancel_monoid α] [covariant_class α α has_mul.mul has_le.le] [contravariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_le.le] (ha : a 1) (hbc : b < c) :
a * b < c
theorem add_lt_of_nonpos_of_lt {α : Type u_1} {a b c : α} [partial_order α] [add_cancel_monoid α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_le.le] (ha : a 0) (hbc : b < c) :
a + b < c
theorem monotone.mul' {α : Type u_1} {β : Type u_2} [preorder β] {f g : β → α} [mul_one_class α] [partial_order α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (hf : monotone f) (hg : monotone g) :
monotone (λ (x : β), (f x) * g x)
theorem monotone.add {α : Type u_1} {β : Type u_2} [preorder β] {f g : β → α} [add_zero_class α] [partial_order α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (hf : monotone f) (hg : monotone g) :
monotone (λ (x : β), f x + g x)
theorem monotone.add_const {α : Type u_1} {β : Type u_2} [preorder β] {f : β → α} [add_zero_class α] [partial_order α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (hf : monotone f) (a : α) :
monotone (λ (x : β), f x + a)
theorem monotone.mul_const' {α : Type u_1} {β : Type u_2} [preorder β] {f : β → α} [mul_one_class α] [partial_order α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (hf : monotone f) (a : α) :
monotone (λ (x : β), (f x) * a)
theorem monotone.const_add {α : Type u_1} {β : Type u_2} [preorder β] {f : β → α} [add_zero_class α] [partial_order α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (hf : monotone f) (a : α) :
monotone (λ (x : β), a + f x)
theorem monotone.const_mul' {α : Type u_1} {β : Type u_2} [preorder β] {f : β → α} [mul_one_class α] [partial_order α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (hf : monotone f) (a : α) :
monotone (λ (x : β), a * f x)
theorem strict_mono.const_add {α : Type u_1} [add_cancel_monoid α] {β : Type u_2} {f : β → α} [partial_order α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_lt.lt] [partial_order β] (hf : strict_mono f) (c : α) :
strict_mono (λ (x : β), c + f x)
theorem strict_mono.const_mul' {α : Type u_1} [cancel_monoid α] {β : Type u_2} {f : β → α} [partial_order α] [covariant_class α α has_mul.mul has_le.le] [contravariant_class α α has_mul.mul has_lt.lt] [partial_order β] (hf : strict_mono f) (c : α) :
strict_mono (λ (x : β), c * f x)
theorem strict_mono.add_const {α : Type u_1} [add_cancel_monoid α] {β : Type u_2} {f : β → α} [partial_order α] [covariant_class α α (function.swap has_add.add) has_le.le] [contravariant_class α α (function.swap has_add.add) has_lt.lt] [partial_order β] (hf : strict_mono f) (c : α) :
strict_mono (λ (x : β), f x + c)
theorem strict_mono.mul_const' {α : Type u_1} [cancel_monoid α] {β : Type u_2} {f : β → α} [partial_order α] [covariant_class α α (function.swap has_mul.mul) has_le.le] [contravariant_class α α (function.swap has_mul.mul) has_lt.lt] [partial_order β] (hf : strict_mono f) (c : α) :
strict_mono (λ (x : β), (f x) * c)
theorem monotone.mul_strict_mono' {α : Type u_1} [cancel_monoid α] [partial_order α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {β : Type u_2} [preorder β] [covariant_class α α has_mul.mul has_le.le] [contravariant_class α α has_mul.mul has_lt.lt] {f g : β → α} (hf : monotone f) (hg : strict_mono g) :
strict_mono (λ (x : β), (f x) * g x)
theorem monotone.add_strict_mono {α : Type u_1} [add_cancel_monoid α] [partial_order α] [covariant_class α α (function.swap has_add.add) has_le.le] {β : Type u_2} [preorder β] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_lt.lt] {f g : β → α} (hf : monotone f) (hg : strict_mono g) :
strict_mono (λ (x : β), f x + g x)
theorem strict_mono.add_monotone {α : Type u_1} [add_cancel_monoid α] {β : Type u_2} {f g : β → α} [partial_order α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] [preorder β] (hf : strict_mono f) (hg : monotone g) :
strict_mono (λ (x : β), f x + g x)
theorem strict_mono.mul_monotone' {α : Type u_1} [cancel_monoid α] {β : Type u_2} {f g : β → α} [partial_order α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] [preorder β] (hf : strict_mono f) (hg : monotone g) :
strict_mono (λ (x : β), (f x) * g x)