Documentation

Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Ordered monoids #

This file develops the basics of ordered monoids.

Implementation details #

Unfortunately, the number of ' appended to lemmas in this file may differ between the multiplicative and the additive version of a lemma. The reason is that we did not want to change existing names in the library.

Remark #

Almost no monoid is actually present in this file: most assumptions have been generalized to Mul or MulOneClass.

theorem add_le_add_left {α : Type u_1} [Add α] [LE α] [AddLeftMono α] {b : α} {c : α} (bc : b c) (a : α) :
a + b a + c
theorem mul_le_mul_left' {α : Type u_1} [Mul α] [LE α] [MulLeftMono α] {b : α} {c : α} (bc : b c) (a : α) :
a * b a * c
theorem le_of_add_le_add_left {α : Type u_1} [Add α] [LE α] [AddLeftReflectLE α] {a : α} {b : α} {c : α} (bc : a + b a + c) :
b c
theorem le_of_mul_le_mul_left' {α : Type u_1} [Mul α] [LE α] [MulLeftReflectLE α] {a : α} {b : α} {c : α} (bc : a * b a * c) :
b c
theorem add_le_add_right {α : Type u_1} [Add α] [LE α] [i : AddRightMono α] {b : α} {c : α} (bc : b c) (a : α) :
b + a c + a
theorem mul_le_mul_right' {α : Type u_1} [Mul α] [LE α] [i : MulRightMono α] {b : α} {c : α} (bc : b c) (a : α) :
b * a c * a
theorem le_of_add_le_add_right {α : Type u_1} [Add α] [LE α] [i : AddRightReflectLE α] {a : α} {b : α} {c : α} (bc : b + a c + a) :
b c
theorem le_of_mul_le_mul_right' {α : Type u_1} [Mul α] [LE α] [i : MulRightReflectLE α] {a : α} {b : α} {c : α} (bc : b * a c * a) :
b c
@[simp]
theorem add_le_add_iff_left {α : Type u_1} [Add α] [LE α] [AddLeftMono α] [AddLeftReflectLE α] (a : α) {b : α} {c : α} :
a + b a + c b c
@[simp]
theorem mul_le_mul_iff_left {α : Type u_1} [Mul α] [LE α] [MulLeftMono α] [MulLeftReflectLE α] (a : α) {b : α} {c : α} :
a * b a * c b c
@[simp]
theorem add_le_add_iff_right {α : Type u_1} [Add α] [LE α] [AddRightMono α] [AddRightReflectLE α] (a : α) {b : α} {c : α} :
b + a c + a b c
@[simp]
theorem mul_le_mul_iff_right {α : Type u_1} [Mul α] [LE α] [MulRightMono α] [MulRightReflectLE α] (a : α) {b : α} {c : α} :
b * a c * a b c
@[simp]
theorem add_lt_add_iff_left {α : Type u_1} [Add α] [LT α] [AddLeftStrictMono α] [AddLeftReflectLT α] (a : α) {b : α} {c : α} :
a + b < a + c b < c
@[simp]
theorem mul_lt_mul_iff_left {α : Type u_1} [Mul α] [LT α] [MulLeftStrictMono α] [MulLeftReflectLT α] (a : α) {b : α} {c : α} :
a * b < a * c b < c
@[simp]
theorem add_lt_add_iff_right {α : Type u_1} [Add α] [LT α] [AddRightStrictMono α] [AddRightReflectLT α] (a : α) {b : α} {c : α} :
b + a < c + a b < c
@[simp]
theorem mul_lt_mul_iff_right {α : Type u_1} [Mul α] [LT α] [MulRightStrictMono α] [MulRightReflectLT α] (a : α) {b : α} {c : α} :
b * a < c * a b < c
theorem add_lt_add_left {α : Type u_1} [Add α] [LT α] [AddLeftStrictMono α] {b : α} {c : α} (bc : b < c) (a : α) :
a + b < a + c
theorem mul_lt_mul_left' {α : Type u_1} [Mul α] [LT α] [MulLeftStrictMono α] {b : α} {c : α} (bc : b < c) (a : α) :
a * b < a * c
theorem lt_of_add_lt_add_left {α : Type u_1} [Add α] [LT α] [AddLeftReflectLT α] {a : α} {b : α} {c : α} (bc : a + b < a + c) :
b < c
theorem lt_of_mul_lt_mul_left' {α : Type u_1} [Mul α] [LT α] [MulLeftReflectLT α] {a : α} {b : α} {c : α} (bc : a * b < a * c) :
b < c
theorem add_lt_add_right {α : Type u_1} [Add α] [LT α] [i : AddRightStrictMono α] {b : α} {c : α} (bc : b < c) (a : α) :
b + a < c + a
theorem mul_lt_mul_right' {α : Type u_1} [Mul α] [LT α] [i : MulRightStrictMono α] {b : α} {c : α} (bc : b < c) (a : α) :
b * a < c * a
theorem lt_of_add_lt_add_right {α : Type u_1} [Add α] [LT α] [i : AddRightReflectLT α] {a : α} {b : α} {c : α} (bc : b + a < c + a) :
b < c
theorem lt_of_mul_lt_mul_right' {α : Type u_1} [Mul α] [LT α] [i : MulRightReflectLT α] {a : α} {b : α} {c : α} (bc : b * a < c * a) :
b < c
theorem add_lt_add_of_lt_of_lt {α : Type u_1} [Add α] [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] {a : α} {b : α} {c : α} {d : α} (h₁ : a < b) (h₂ : c < d) :
a + c < b + d
theorem mul_lt_mul_of_lt_of_lt {α : Type u_1} [Mul α] [Preorder α] [MulLeftStrictMono α] [MulRightStrictMono α] {a : α} {b : α} {c : α} {d : α} (h₁ : a < b) (h₂ : c < d) :
a * c < b * d
theorem add_lt_add {α : Type u_1} [Add α] [Preorder α] [AddLeftStrictMono α] [AddRightStrictMono α] {a : α} {b : α} {c : α} {d : α} (h₁ : a < b) (h₂ : c < d) :
a + c < b + d

Alias of add_lt_add_of_lt_of_lt.

theorem add_lt_add_of_le_of_lt {α : Type u_1} [Add α] [Preorder α] [AddLeftStrictMono α] [AddRightMono α] {a : α} {b : α} {c : α} {d : α} (h₁ : a b) (h₂ : c < d) :
a + c < b + d
theorem mul_lt_mul_of_le_of_lt {α : Type u_1} [Mul α] [Preorder α] [MulLeftStrictMono α] [MulRightMono α] {a : α} {b : α} {c : α} {d : α} (h₁ : a b) (h₂ : c < d) :
a * c < b * d
theorem add_lt_add_of_lt_of_le {α : Type u_1} [Add α] [Preorder α] [AddLeftMono α] [AddRightStrictMono α] {a : α} {b : α} {c : α} {d : α} (h₁ : a < b) (h₂ : c d) :
a + c < b + d
theorem mul_lt_mul_of_lt_of_le {α : Type u_1} [Mul α] [Preorder α] [MulLeftMono α] [MulRightStrictMono α] {a : α} {b : α} {c : α} {d : α} (h₁ : a < b) (h₂ : c d) :
a * c < b * d
theorem Left.add_lt_add {α : Type u_1} [Add α] [Preorder α] [AddLeftStrictMono α] [AddRightMono α] {a : α} {b : α} {c : α} {d : α} (h₁ : a < b) (h₂ : c < d) :
a + c < b + d

Only assumes left strict covariance

theorem Left.mul_lt_mul {α : Type u_1} [Mul α] [Preorder α] [MulLeftStrictMono α] [MulRightMono α] {a : α} {b : α} {c : α} {d : α} (h₁ : a < b) (h₂ : c < d) :
a * c < b * d

Only assumes left strict covariance.

theorem Right.add_lt_add {α : Type u_1} [Add α] [Preorder α] [AddLeftMono α] [AddRightStrictMono α] {a : α} {b : α} {c : α} {d : α} (h₁ : a < b) (h₂ : c < d) :
a + c < b + d

Only assumes right strict covariance

theorem Right.mul_lt_mul {α : Type u_1} [Mul α] [Preorder α] [MulLeftMono α] [MulRightStrictMono α] {a : α} {b : α} {c : α} {d : α} (h₁ : a < b) (h₂ : c < d) :
a * c < b * d

Only assumes right strict covariance.

theorem add_le_add {α : Type u_1} [Add α] [Preorder α] [AddLeftMono α] [AddRightMono α] {a : α} {b : α} {c : α} {d : α} (h₁ : a b) (h₂ : c d) :
a + c b + d
theorem mul_le_mul' {α : Type u_1} [Mul α] [Preorder α] [MulLeftMono α] [MulRightMono α] {a : α} {b : α} {c : α} {d : α} (h₁ : a b) (h₂ : c d) :
a * c b * d
theorem add_le_add_three {α : Type u_1} [Add α] [Preorder α] [AddLeftMono α] [AddRightMono α] {a : α} {b : α} {c : α} {d : α} {e : α} {f : α} (h₁ : a d) (h₂ : b e) (h₃ : c f) :
a + b + c d + e + f
theorem mul_le_mul_three {α : Type u_1} [Mul α] [Preorder α] [MulLeftMono α] [MulRightMono α] {a : α} {b : α} {c : α} {d : α} {e : α} {f : α} (h₁ : a d) (h₂ : b e) (h₃ : c f) :
a * b * c d * e * f
theorem add_lt_of_add_lt_left {α : Type u_1} [Add α] [Preorder α] [AddLeftMono α] {a : α} {b : α} {c : α} {d : α} (h : a + b < c) (hle : d b) :
a + d < c
theorem mul_lt_of_mul_lt_left {α : Type u_1} [Mul α] [Preorder α] [MulLeftMono α] {a : α} {b : α} {c : α} {d : α} (h : a * b < c) (hle : d b) :
a * d < c
theorem add_le_of_add_le_left {α : Type u_1} [Add α] [Preorder α] [AddLeftMono α] {a : α} {b : α} {c : α} {d : α} (h : a + b c) (hle : d b) :
a + d c
theorem mul_le_of_mul_le_left {α : Type u_1} [Mul α] [Preorder α] [MulLeftMono α] {a : α} {b : α} {c : α} {d : α} (h : a * b c) (hle : d b) :
a * d c
theorem add_lt_of_add_lt_right {α : Type u_1} [Add α] [Preorder α] [AddRightMono α] {a : α} {b : α} {c : α} {d : α} (h : a + b < c) (hle : d a) :
d + b < c
theorem mul_lt_of_mul_lt_right {α : Type u_1} [Mul α] [Preorder α] [MulRightMono α] {a : α} {b : α} {c : α} {d : α} (h : a * b < c) (hle : d a) :
d * b < c
theorem add_le_of_add_le_right {α : Type u_1} [Add α] [Preorder α] [AddRightMono α] {a : α} {b : α} {c : α} {d : α} (h : a + b c) (hle : d a) :
d + b c
theorem mul_le_of_mul_le_right {α : Type u_1} [Mul α] [Preorder α] [MulRightMono α] {a : α} {b : α} {c : α} {d : α} (h : a * b c) (hle : d a) :
d * b c
theorem lt_add_of_lt_add_left {α : Type u_1} [Add α] [Preorder α] [AddLeftMono α] {a : α} {b : α} {c : α} {d : α} (h : a < b + c) (hle : c d) :
a < b + d
theorem lt_mul_of_lt_mul_left {α : Type u_1} [Mul α] [Preorder α] [MulLeftMono α] {a : α} {b : α} {c : α} {d : α} (h : a < b * c) (hle : c d) :
a < b * d
theorem le_add_of_le_add_left {α : Type u_1} [Add α] [Preorder α] [AddLeftMono α] {a : α} {b : α} {c : α} {d : α} (h : a b + c) (hle : c d) :
a b + d
theorem le_mul_of_le_mul_left {α : Type u_1} [Mul α] [Preorder α] [MulLeftMono α] {a : α} {b : α} {c : α} {d : α} (h : a b * c) (hle : c d) :
a b * d
theorem lt_add_of_lt_add_right {α : Type u_1} [Add α] [Preorder α] [AddRightMono α] {a : α} {b : α} {c : α} {d : α} (h : a < b + c) (hle : b d) :
a < d + c
theorem lt_mul_of_lt_mul_right {α : Type u_1} [Mul α] [Preorder α] [MulRightMono α] {a : α} {b : α} {c : α} {d : α} (h : a < b * c) (hle : b d) :
a < d * c
theorem le_add_of_le_add_right {α : Type u_1} [Add α] [Preorder α] [AddRightMono α] {a : α} {b : α} {c : α} {d : α} (h : a b + c) (hle : b d) :
a d + c
theorem le_mul_of_le_mul_right {α : Type u_1} [Mul α] [Preorder α] [MulRightMono α] {a : α} {b : α} {c : α} {d : α} (h : a b * c) (hle : b d) :
a d * c
theorem add_left_cancel'' {α : Type u_1} [Add α] [PartialOrder α] [AddLeftReflectLE α] {a : α} {b : α} {c : α} (h : a + b = a + c) :
b = c
theorem mul_left_cancel'' {α : Type u_1} [Mul α] [PartialOrder α] [MulLeftReflectLE α] {a : α} {b : α} {c : α} (h : a * b = a * c) :
b = c
theorem add_right_cancel'' {α : Type u_1} [Add α] [PartialOrder α] [AddRightReflectLE α] {a : α} {b : α} {c : α} (h : a + b = c + b) :
a = c
theorem mul_right_cancel'' {α : Type u_1} [Mul α] [PartialOrder α] [MulRightReflectLE α] {a : α} {b : α} {c : α} (h : a * b = c * b) :
a = c
theorem add_le_add_iff_of_ge {α : Type u_1} [Add α] [PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (ha : a₁ a₂) (hb : b₁ b₂) :
a₂ + b₂ a₁ + b₁ a₁ = a₂ b₁ = b₂
theorem mul_le_mul_iff_of_ge {α : Type u_1} [Mul α] [PartialOrder α] [MulLeftStrictMono α] [MulRightStrictMono α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (ha : a₁ a₂) (hb : b₁ b₂) :
a₂ * b₂ a₁ * b₁ a₁ = a₂ b₁ = b₂
theorem add_eq_add_iff_eq_and_eq {α : Type u_1} [Add α] [PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] {a : α} {b : α} {c : α} {d : α} (hac : a c) (hbd : b d) :
a + b = c + d a = c b = d
theorem mul_eq_mul_iff_eq_and_eq {α : Type u_1} [Mul α] [PartialOrder α] [MulLeftStrictMono α] [MulRightStrictMono α] {a : α} {b : α} {c : α} {d : α} (hac : a c) (hbd : b d) :
a * b = c * d a = c b = d
theorem min_lt_max_of_add_lt_add {α : Type u_1} [Add α] [LinearOrder α] {a : α} {b : α} {c : α} {d : α} [AddLeftMono α] [AddRightMono α] (h : a + b < c + d) :
min a b < max c d
theorem min_lt_max_of_mul_lt_mul {α : Type u_1} [Mul α] [LinearOrder α] {a : α} {b : α} {c : α} {d : α} [MulLeftMono α] [MulRightMono α] (h : a * b < c * d) :
min a b < max c d
theorem Left.min_le_max_of_add_le_add {α : Type u_1} [Add α] [LinearOrder α] {a : α} {b : α} {c : α} {d : α} [AddLeftStrictMono α] [AddRightMono α] (h : a + b c + d) :
min a b max c d
theorem Left.min_le_max_of_mul_le_mul {α : Type u_1} [Mul α] [LinearOrder α] {a : α} {b : α} {c : α} {d : α} [MulLeftStrictMono α] [MulRightMono α] (h : a * b c * d) :
min a b max c d
theorem Right.min_le_max_of_add_le_add {α : Type u_1} [Add α] [LinearOrder α] {a : α} {b : α} {c : α} {d : α} [AddLeftMono α] [AddRightStrictMono α] (h : a + b c + d) :
min a b max c d
theorem Right.min_le_max_of_mul_le_mul {α : Type u_1} [Mul α] [LinearOrder α] {a : α} {b : α} {c : α} {d : α} [MulLeftMono α] [MulRightStrictMono α] (h : a * b c * d) :
min a b max c d
theorem min_le_max_of_add_le_add {α : Type u_1} [Add α] [LinearOrder α] {a : α} {b : α} {c : α} {d : α} [AddLeftStrictMono α] [AddRightStrictMono α] (h : a + b c + d) :
min a b max c d
theorem min_le_max_of_mul_le_mul {α : Type u_1} [Mul α] [LinearOrder α] {a : α} {b : α} {c : α} {d : α} [MulLeftStrictMono α] [MulRightStrictMono α] (h : a * b c * d) :
min a b max c d
theorem max_add_add_le_max_add_max {α : Type u_1} [Add α] [LinearOrder α] [AddLeftMono α] [AddRightMono α] {a : α} {b : α} {c : α} {d : α} :
max (a + b) (c + d) max a c + max b d
theorem max_mul_mul_le_max_mul_max' {α : Type u_1} [Mul α] [LinearOrder α] [MulLeftMono α] [MulRightMono α] {a : α} {b : α} {c : α} {d : α} :
max (a * b) (c * d) max a c * max b d
theorem min_add_min_le_min_add_add {α : Type u_1} [Add α] [LinearOrder α] [AddLeftMono α] [AddRightMono α] {a : α} {b : α} {c : α} {d : α} :
min a c + min b d min (a + b) (c + d)
theorem min_mul_min_le_min_mul_mul' {α : Type u_1} [Mul α] [LinearOrder α] [MulLeftMono α] [MulRightMono α] {a : α} {b : α} {c : α} {d : α} :
min a c * min b d min (a * b) (c * d)
theorem le_add_of_nonneg_right {α : Type u_1} [AddZeroClass α] [LE α] [AddLeftMono α] {a : α} {b : α} (h : 0 b) :
a a + b
theorem le_mul_of_one_le_right' {α : Type u_1} [MulOneClass α] [LE α] [MulLeftMono α] {a : α} {b : α} (h : 1 b) :
a a * b
theorem add_le_of_nonpos_right {α : Type u_1} [AddZeroClass α] [LE α] [AddLeftMono α] {a : α} {b : α} (h : b 0) :
a + b a
theorem mul_le_of_le_one_right' {α : Type u_1} [MulOneClass α] [LE α] [MulLeftMono α] {a : α} {b : α} (h : b 1) :
a * b a
theorem le_add_of_nonneg_left {α : Type u_1} [AddZeroClass α] [LE α] [AddRightMono α] {a : α} {b : α} (h : 0 b) :
a b + a
theorem le_mul_of_one_le_left' {α : Type u_1} [MulOneClass α] [LE α] [MulRightMono α] {a : α} {b : α} (h : 1 b) :
a b * a
theorem add_le_of_nonpos_left {α : Type u_1} [AddZeroClass α] [LE α] [AddRightMono α] {a : α} {b : α} (h : b 0) :
b + a a
theorem mul_le_of_le_one_left' {α : Type u_1} [MulOneClass α] [LE α] [MulRightMono α] {a : α} {b : α} (h : b 1) :
b * a a
theorem nonneg_of_le_add_right {α : Type u_1} [AddZeroClass α] [LE α] [AddLeftReflectLE α] {a : α} {b : α} (h : a a + b) :
0 b
theorem one_le_of_le_mul_right {α : Type u_1} [MulOneClass α] [LE α] [MulLeftReflectLE α] {a : α} {b : α} (h : a a * b) :
1 b
theorem nonpos_of_add_le_right {α : Type u_1} [AddZeroClass α] [LE α] [AddLeftReflectLE α] {a : α} {b : α} (h : a + b a) :
b 0
theorem le_one_of_mul_le_right {α : Type u_1} [MulOneClass α] [LE α] [MulLeftReflectLE α] {a : α} {b : α} (h : a * b a) :
b 1
theorem nonneg_of_le_add_left {α : Type u_1} [AddZeroClass α] [LE α] [AddRightReflectLE α] {a : α} {b : α} (h : b a + b) :
0 a
theorem one_le_of_le_mul_left {α : Type u_1} [MulOneClass α] [LE α] [MulRightReflectLE α] {a : α} {b : α} (h : b a * b) :
1 a
theorem nonpos_of_add_le_left {α : Type u_1} [AddZeroClass α] [LE α] [AddRightReflectLE α] {a : α} {b : α} (h : a + b b) :
a 0
theorem le_one_of_mul_le_left {α : Type u_1} [MulOneClass α] [LE α] [MulRightReflectLE α] {a : α} {b : α} (h : a * b b) :
a 1
@[simp]
theorem le_add_iff_nonneg_right {α : Type u_1} [AddZeroClass α] [LE α] [AddLeftMono α] [AddLeftReflectLE α] (a : α) {b : α} :
a a + b 0 b
@[simp]
theorem le_mul_iff_one_le_right' {α : Type u_1} [MulOneClass α] [LE α] [MulLeftMono α] [MulLeftReflectLE α] (a : α) {b : α} :
a a * b 1 b
@[simp]
theorem le_add_iff_nonneg_left {α : Type u_1} [AddZeroClass α] [LE α] [AddRightMono α] [AddRightReflectLE α] (a : α) {b : α} :
a b + a 0 b
@[simp]
theorem le_mul_iff_one_le_left' {α : Type u_1} [MulOneClass α] [LE α] [MulRightMono α] [MulRightReflectLE α] (a : α) {b : α} :
a b * a 1 b
@[simp]
theorem add_le_iff_nonpos_right {α : Type u_1} [AddZeroClass α] [LE α] [AddLeftMono α] [AddLeftReflectLE α] (a : α) {b : α} :
a + b a b 0
@[simp]
theorem mul_le_iff_le_one_right' {α : Type u_1} [MulOneClass α] [LE α] [MulLeftMono α] [MulLeftReflectLE α] (a : α) {b : α} :
a * b a b 1
@[simp]
theorem add_le_iff_nonpos_left {α : Type u_1} [AddZeroClass α] [LE α] [AddRightMono α] [AddRightReflectLE α] {a : α} {b : α} :
a + b b a 0
@[simp]
theorem mul_le_iff_le_one_left' {α : Type u_1} [MulOneClass α] [LE α] [MulRightMono α] [MulRightReflectLE α] {a : α} {b : α} :
a * b b a 1
theorem lt_add_of_pos_right {α : Type u_1} [AddZeroClass α] [LT α] [AddLeftStrictMono α] (a : α) {b : α} (h : 0 < b) :
a < a + b
theorem lt_mul_of_one_lt_right' {α : Type u_1} [MulOneClass α] [LT α] [MulLeftStrictMono α] (a : α) {b : α} (h : 1 < b) :
a < a * b
theorem add_lt_of_neg_right {α : Type u_1} [AddZeroClass α] [LT α] [AddLeftStrictMono α] (a : α) {b : α} (h : b < 0) :
a + b < a
theorem mul_lt_of_lt_one_right' {α : Type u_1} [MulOneClass α] [LT α] [MulLeftStrictMono α] (a : α) {b : α} (h : b < 1) :
a * b < a
theorem lt_add_of_pos_left {α : Type u_1} [AddZeroClass α] [LT α] [AddRightStrictMono α] (a : α) {b : α} (h : 0 < b) :
a < b + a
theorem lt_mul_of_one_lt_left' {α : Type u_1} [MulOneClass α] [LT α] [MulRightStrictMono α] (a : α) {b : α} (h : 1 < b) :
a < b * a
theorem add_lt_of_neg_left {α : Type u_1} [AddZeroClass α] [LT α] [AddRightStrictMono α] (a : α) {b : α} (h : b < 0) :
b + a < a
theorem mul_lt_of_lt_one_left' {α : Type u_1} [MulOneClass α] [LT α] [MulRightStrictMono α] (a : α) {b : α} (h : b < 1) :
b * a < a
theorem pos_of_lt_add_right {α : Type u_1} [AddZeroClass α] [LT α] [AddLeftReflectLT α] {a : α} {b : α} (h : a < a + b) :
0 < b
theorem one_lt_of_lt_mul_right {α : Type u_1} [MulOneClass α] [LT α] [MulLeftReflectLT α] {a : α} {b : α} (h : a < a * b) :
1 < b
theorem neg_of_add_lt_right {α : Type u_1} [AddZeroClass α] [LT α] [AddLeftReflectLT α] {a : α} {b : α} (h : a + b < a) :
b < 0
theorem lt_one_of_mul_lt_right {α : Type u_1} [MulOneClass α] [LT α] [MulLeftReflectLT α] {a : α} {b : α} (h : a * b < a) :
b < 1
theorem pos_of_lt_add_left {α : Type u_1} [AddZeroClass α] [LT α] [AddRightReflectLT α] {a : α} {b : α} (h : b < a + b) :
0 < a
theorem one_lt_of_lt_mul_left {α : Type u_1} [MulOneClass α] [LT α] [MulRightReflectLT α] {a : α} {b : α} (h : b < a * b) :
1 < a
theorem neg_of_add_lt_left {α : Type u_1} [AddZeroClass α] [LT α] [AddRightReflectLT α] {a : α} {b : α} (h : a + b < b) :
a < 0
theorem lt_one_of_mul_lt_left {α : Type u_1} [MulOneClass α] [LT α] [MulRightReflectLT α] {a : α} {b : α} (h : a * b < b) :
a < 1
@[simp]
theorem lt_add_iff_pos_right {α : Type u_1} [AddZeroClass α] [LT α] [AddLeftStrictMono α] [AddLeftReflectLT α] (a : α) {b : α} :
a < a + b 0 < b
@[simp]
theorem lt_mul_iff_one_lt_right' {α : Type u_1} [MulOneClass α] [LT α] [MulLeftStrictMono α] [MulLeftReflectLT α] (a : α) {b : α} :
a < a * b 1 < b
@[simp]
theorem lt_add_iff_pos_left {α : Type u_1} [AddZeroClass α] [LT α] [AddRightStrictMono α] [AddRightReflectLT α] (a : α) {b : α} :
a < b + a 0 < b
@[simp]
theorem lt_mul_iff_one_lt_left' {α : Type u_1} [MulOneClass α] [LT α] [MulRightStrictMono α] [MulRightReflectLT α] (a : α) {b : α} :
a < b * a 1 < b
@[simp]
theorem add_lt_iff_neg_left {α : Type u_1} [AddZeroClass α] [LT α] [AddLeftStrictMono α] [AddLeftReflectLT α] {a : α} {b : α} :
a + b < a b < 0
@[simp]
theorem mul_lt_iff_lt_one_left' {α : Type u_1} [MulOneClass α] [LT α] [MulLeftStrictMono α] [MulLeftReflectLT α] {a : α} {b : α} :
a * b < a b < 1
@[simp]
theorem add_lt_iff_neg_right {α : Type u_1} [AddZeroClass α] [LT α] [AddRightStrictMono α] [AddRightReflectLT α] {a : α} (b : α) :
a + b < b a < 0
@[simp]
theorem mul_lt_iff_lt_one_right' {α : Type u_1} [MulOneClass α] [LT α] [MulRightStrictMono α] [MulRightReflectLT α] {a : α} (b : α) :
a * b < b a < 1

Lemmas of the form b ≤ c → a ≤ 1 → b * a ≤ c, which assume left covariance.

theorem add_le_of_le_of_nonpos {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a : α} {b : α} {c : α} (hbc : b c) (ha : a 0) :
b + a c
theorem mul_le_of_le_of_le_one {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftMono α] {a : α} {b : α} {c : α} (hbc : b c) (ha : a 1) :
b * a c
theorem add_lt_of_le_of_neg {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] {a : α} {b : α} {c : α} (hbc : b c) (ha : a < 0) :
b + a < c
theorem mul_lt_of_le_of_lt_one {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftStrictMono α] {a : α} {b : α} {c : α} (hbc : b c) (ha : a < 1) :
b * a < c
theorem add_lt_of_lt_of_nonpos {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a : α} {b : α} {c : α} (hbc : b < c) (ha : a 0) :
b + a < c
theorem mul_lt_of_lt_of_le_one {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftMono α] {a : α} {b : α} {c : α} (hbc : b < c) (ha : a 1) :
b * a < c
theorem add_lt_of_lt_of_neg {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] {a : α} {b : α} {c : α} (hbc : b < c) (ha : a < 0) :
b + a < c
theorem mul_lt_of_lt_of_lt_one {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftStrictMono α] {a : α} {b : α} {c : α} (hbc : b < c) (ha : a < 1) :
b * a < c
theorem add_lt_of_lt_of_neg' {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a : α} {b : α} {c : α} (hbc : b < c) (ha : a < 0) :
b + a < c
theorem mul_lt_of_lt_of_lt_one' {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftMono α] {a : α} {b : α} {c : α} (hbc : b < c) (ha : a < 1) :
b * a < c
theorem Left.add_nonpos {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a : α} {b : α} (ha : a 0) (hb : b 0) :
a + b 0

Assumes left covariance. The lemma assuming right covariance is Right.add_nonpos.

theorem Left.mul_le_one {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftMono α] {a : α} {b : α} (ha : a 1) (hb : b 1) :
a * b 1

Assumes left covariance. The lemma assuming right covariance is Right.mul_le_one.

theorem Left.add_neg_of_nonpos_of_neg {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] {a : α} {b : α} (ha : a 0) (hb : b < 0) :
a + b < 0

Assumes left covariance. The lemma assuming right covariance is Right.add_neg_of_nonpos_of_neg.

theorem Left.mul_lt_one_of_le_of_lt {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftStrictMono α] {a : α} {b : α} (ha : a 1) (hb : b < 1) :
a * b < 1

Assumes left covariance. The lemma assuming right covariance is Right.mul_lt_one_of_le_of_lt.

theorem Left.add_neg_of_neg_of_nonpos {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a : α} {b : α} (ha : a < 0) (hb : b 0) :
a + b < 0

Assumes left covariance. The lemma assuming right covariance is Right.add_neg_of_neg_of_nonpos.

theorem Left.mul_lt_one_of_lt_of_le {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftMono α] {a : α} {b : α} (ha : a < 1) (hb : b 1) :
a * b < 1

Assumes left covariance. The lemma assuming right covariance is Right.mul_lt_one_of_lt_of_le.

theorem Left.add_neg {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] {a : α} {b : α} (ha : a < 0) (hb : b < 0) :
a + b < 0

Assumes left covariance. The lemma assuming right covariance is Right.add_neg.

theorem Left.mul_lt_one {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftStrictMono α] {a : α} {b : α} (ha : a < 1) (hb : b < 1) :
a * b < 1

Assumes left covariance. The lemma assuming right covariance is Right.mul_lt_one.

theorem Left.add_neg' {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a : α} {b : α} (ha : a < 0) (hb : b < 0) :
a + b < 0

Assumes left covariance. The lemma assuming right covariance is Right.add_neg'.

theorem Left.mul_lt_one' {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftMono α] {a : α} {b : α} (ha : a < 1) (hb : b < 1) :
a * b < 1

Assumes left covariance. The lemma assuming right covariance is Right.mul_lt_one'.

Lemmas of the form b ≤ c → 1 ≤ a → b ≤ c * a, which assume left covariance.

theorem le_add_of_le_of_nonneg {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a : α} {b : α} {c : α} (hbc : b c) (ha : 0 a) :
b c + a
theorem le_mul_of_le_of_one_le {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftMono α] {a : α} {b : α} {c : α} (hbc : b c) (ha : 1 a) :
b c * a
theorem lt_add_of_le_of_pos {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] {a : α} {b : α} {c : α} (hbc : b c) (ha : 0 < a) :
b < c + a
theorem lt_mul_of_le_of_one_lt {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftStrictMono α] {a : α} {b : α} {c : α} (hbc : b c) (ha : 1 < a) :
b < c * a
theorem lt_add_of_lt_of_nonneg {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a : α} {b : α} {c : α} (hbc : b < c) (ha : 0 a) :
b < c + a
theorem lt_mul_of_lt_of_one_le {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftMono α] {a : α} {b : α} {c : α} (hbc : b < c) (ha : 1 a) :
b < c * a
theorem lt_add_of_lt_of_pos {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] {a : α} {b : α} {c : α} (hbc : b < c) (ha : 0 < a) :
b < c + a
theorem lt_mul_of_lt_of_one_lt {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftStrictMono α] {a : α} {b : α} {c : α} (hbc : b < c) (ha : 1 < a) :
b < c * a
theorem lt_add_of_lt_of_pos' {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a : α} {b : α} {c : α} (hbc : b < c) (ha : 0 < a) :
b < c + a
theorem lt_mul_of_lt_of_one_lt' {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftMono α] {a : α} {b : α} {c : α} (hbc : b < c) (ha : 1 < a) :
b < c * a
theorem Left.add_nonneg {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a : α} {b : α} (ha : 0 a) (hb : 0 b) :
0 a + b

Assumes left covariance. The lemma assuming right covariance is Right.add_nonneg.

theorem Left.one_le_mul {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftMono α] {a : α} {b : α} (ha : 1 a) (hb : 1 b) :
1 a * b

Assumes left covariance. The lemma assuming right covariance is Right.one_le_mul.

theorem Left.add_pos_of_nonneg_of_pos {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] {a : α} {b : α} (ha : 0 a) (hb : 0 < b) :
0 < a + 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} [MulOneClass α] [Preorder α] [MulLeftStrictMono α] {a : α} {b : α} (ha : 1 a) (hb : 1 < b) :
1 < a * 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} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a : α} {b : α} (ha : 0 < a) (hb : 0 b) :
0 < a + 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} [MulOneClass α] [Preorder α] [MulLeftMono α] {a : α} {b : α} (ha : 1 < a) (hb : 1 b) :
1 < a * b

Assumes left covariance. The lemma assuming right covariance is Right.one_lt_mul_of_lt_of_le.

theorem Left.add_pos {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] {a : α} {b : α} (ha : 0 < a) (hb : 0 < b) :
0 < a + b

Assumes left covariance. The lemma assuming right covariance is Right.add_pos.

theorem Left.one_lt_mul {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftStrictMono α] {a : α} {b : α} (ha : 1 < a) (hb : 1 < b) :
1 < a * b

Assumes left covariance. The lemma assuming right covariance is Right.one_lt_mul.

theorem Left.add_pos' {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a : α} {b : α} (ha : 0 < a) (hb : 0 < b) :
0 < a + b

Assumes left covariance. The lemma assuming right covariance is Right.add_pos'.

theorem Left.one_lt_mul' {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftMono α] {a : α} {b : α} (ha : 1 < a) (hb : 1 < b) :
1 < a * 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} [AddZeroClass α] [Preorder α] [AddRightMono α] {a : α} {b : α} {c : α} (ha : a 0) (hbc : b c) :
a + b c
theorem mul_le_of_le_one_of_le {α : Type u_1} [MulOneClass α] [Preorder α] [MulRightMono α] {a : α} {b : α} {c : α} (ha : a 1) (hbc : b c) :
a * b c
theorem add_lt_of_neg_of_le {α : Type u_1} [AddZeroClass α] [Preorder α] [AddRightStrictMono α] {a : α} {b : α} {c : α} (ha : a < 0) (hbc : b c) :
a + b < c
theorem mul_lt_of_lt_one_of_le {α : Type u_1} [MulOneClass α] [Preorder α] [MulRightStrictMono α] {a : α} {b : α} {c : α} (ha : a < 1) (hbc : b c) :
a * b < c
theorem add_lt_of_nonpos_of_lt {α : Type u_1} [AddZeroClass α] [Preorder α] [AddRightMono α] {a : α} {b : α} {c : α} (ha : a 0) (hb : b < c) :
a + b < c
theorem mul_lt_of_le_one_of_lt {α : Type u_1} [MulOneClass α] [Preorder α] [MulRightMono α] {a : α} {b : α} {c : α} (ha : a 1) (hb : b < c) :
a * b < c
theorem add_lt_of_neg_of_lt {α : Type u_1} [AddZeroClass α] [Preorder α] [AddRightStrictMono α] {a : α} {b : α} {c : α} (ha : a < 0) (hb : b < c) :
a + b < c
theorem mul_lt_of_lt_one_of_lt {α : Type u_1} [MulOneClass α] [Preorder α] [MulRightStrictMono α] {a : α} {b : α} {c : α} (ha : a < 1) (hb : b < c) :
a * b < c
theorem add_lt_of_neg_of_lt' {α : Type u_1} [AddZeroClass α] [Preorder α] [AddRightMono α] {a : α} {b : α} {c : α} (ha : a < 0) (hbc : b < c) :
a + b < c
theorem mul_lt_of_lt_one_of_lt' {α : Type u_1} [MulOneClass α] [Preorder α] [MulRightMono α] {a : α} {b : α} {c : α} (ha : a < 1) (hbc : b < c) :
a * b < c
theorem Right.add_nonpos {α : Type u_1} [AddZeroClass α] [Preorder α] [AddRightMono α] {a : α} {b : α} (ha : a 0) (hb : b 0) :
a + b 0

Assumes right covariance. The lemma assuming left covariance is Left.add_nonpos.

theorem Right.mul_le_one {α : Type u_1} [MulOneClass α] [Preorder α] [MulRightMono α] {a : α} {b : α} (ha : a 1) (hb : b 1) :
a * b 1

Assumes right covariance. The lemma assuming left covariance is Left.mul_le_one.

theorem Right.add_neg_of_neg_of_nonpos {α : Type u_1} [AddZeroClass α] [Preorder α] [AddRightStrictMono α] {a : α} {b : α} (ha : a < 0) (hb : b 0) :
a + 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} [MulOneClass α] [Preorder α] [MulRightStrictMono α] {a : α} {b : α} (ha : a < 1) (hb : b 1) :
a * b < 1

Assumes right covariance. The lemma assuming left covariance is Left.mul_lt_one_of_lt_of_le.

theorem Right.add_neg_of_nonpos_of_neg {α : Type u_1} [AddZeroClass α] [Preorder α] [AddRightMono α] {a : α} {b : α} (ha : a 0) (hb : b < 0) :
a + b < 0

Assumes right covariance. The lemma assuming left covariance is Left.add_neg_of_nonpos_of_neg.

theorem Right.mul_lt_one_of_le_of_lt {α : Type u_1} [MulOneClass α] [Preorder α] [MulRightMono α] {a : α} {b : α} (ha : a 1) (hb : b < 1) :
a * b < 1

Assumes right covariance. The lemma assuming left covariance is Left.mul_lt_one_of_le_of_lt.

theorem Right.add_neg {α : Type u_1} [AddZeroClass α] [Preorder α] [AddRightStrictMono α] {a : α} {b : α} (ha : a < 0) (hb : b < 0) :
a + b < 0

Assumes right covariance. The lemma assuming left covariance is Left.add_neg.

theorem Right.mul_lt_one {α : Type u_1} [MulOneClass α] [Preorder α] [MulRightStrictMono α] {a : α} {b : α} (ha : a < 1) (hb : b < 1) :
a * b < 1

Assumes right covariance. The lemma assuming left covariance is Left.mul_lt_one.

theorem Right.add_neg' {α : Type u_1} [AddZeroClass α] [Preorder α] [AddRightMono α] {a : α} {b : α} (ha : a < 0) (hb : b < 0) :
a + b < 0

Assumes right covariance. The lemma assuming left covariance is Left.add_neg'.

theorem Right.mul_lt_one' {α : Type u_1} [MulOneClass α] [Preorder α] [MulRightMono α] {a : α} {b : α} (ha : a < 1) (hb : b < 1) :
a * 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} [AddZeroClass α] [Preorder α] [AddRightMono α] {a : α} {b : α} {c : α} (ha : 0 a) (hbc : b c) :
b a + c
theorem le_mul_of_one_le_of_le {α : Type u_1} [MulOneClass α] [Preorder α] [MulRightMono α] {a : α} {b : α} {c : α} (ha : 1 a) (hbc : b c) :
b a * c
theorem lt_add_of_pos_of_le {α : Type u_1} [AddZeroClass α] [Preorder α] [AddRightStrictMono α] {a : α} {b : α} {c : α} (ha : 0 < a) (hbc : b c) :
b < a + c
theorem lt_mul_of_one_lt_of_le {α : Type u_1} [MulOneClass α] [Preorder α] [MulRightStrictMono α] {a : α} {b : α} {c : α} (ha : 1 < a) (hbc : b c) :
b < a * c
theorem lt_add_of_nonneg_of_lt {α : Type u_1} [AddZeroClass α] [Preorder α] [AddRightMono α] {a : α} {b : α} {c : α} (ha : 0 a) (hbc : b < c) :
b < a + c
theorem lt_mul_of_one_le_of_lt {α : Type u_1} [MulOneClass α] [Preorder α] [MulRightMono α] {a : α} {b : α} {c : α} (ha : 1 a) (hbc : b < c) :
b < a * c
theorem lt_add_of_pos_of_lt {α : Type u_1} [AddZeroClass α] [Preorder α] [AddRightStrictMono α] {a : α} {b : α} {c : α} (ha : 0 < a) (hbc : b < c) :
b < a + c
theorem lt_mul_of_one_lt_of_lt {α : Type u_1} [MulOneClass α] [Preorder α] [MulRightStrictMono α] {a : α} {b : α} {c : α} (ha : 1 < a) (hbc : b < c) :
b < a * c
theorem lt_add_of_pos_of_lt' {α : Type u_1} [AddZeroClass α] [Preorder α] [AddRightMono α] {a : α} {b : α} {c : α} (ha : 0 < a) (hbc : b < c) :
b < a + c
theorem lt_mul_of_one_lt_of_lt' {α : Type u_1} [MulOneClass α] [Preorder α] [MulRightMono α] {a : α} {b : α} {c : α} (ha : 1 < a) (hbc : b < c) :
b < a * c
theorem Right.add_nonneg {α : Type u_1} [AddZeroClass α] [Preorder α] [AddRightMono α] {a : α} {b : α} (ha : 0 a) (hb : 0 b) :
0 a + b

Assumes right covariance. The lemma assuming left covariance is Left.add_nonneg.

theorem Right.one_le_mul {α : Type u_1} [MulOneClass α] [Preorder α] [MulRightMono α] {a : α} {b : α} (ha : 1 a) (hb : 1 b) :
1 a * 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} [AddZeroClass α] [Preorder α] [AddRightStrictMono α] {a : α} {b : α} (ha : 0 < a) (hb : 0 b) :
0 < a + 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} [MulOneClass α] [Preorder α] [MulRightStrictMono α] {a : α} {b : α} (ha : 1 < a) (hb : 1 b) :
1 < a * 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} [AddZeroClass α] [Preorder α] [AddRightMono α] {a : α} {b : α} (ha : 0 a) (hb : 0 < b) :
0 < a + 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} [MulOneClass α] [Preorder α] [MulRightMono α] {a : α} {b : α} (ha : 1 a) (hb : 1 < b) :
1 < a * 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} [AddZeroClass α] [Preorder α] [AddRightStrictMono α] {a : α} {b : α} (ha : 0 < a) (hb : 0 < b) :
0 < a + b

Assumes right covariance. The lemma assuming left covariance is Left.add_pos.

theorem Right.one_lt_mul {α : Type u_1} [MulOneClass α] [Preorder α] [MulRightStrictMono α] {a : α} {b : α} (ha : 1 < a) (hb : 1 < b) :
1 < a * b

Assumes right covariance. The lemma assuming left covariance is Left.one_lt_mul.

theorem Right.add_pos' {α : Type u_1} [AddZeroClass α] [Preorder α] [AddRightMono α] {a : α} {b : α} (ha : 0 < a) (hb : 0 < b) :
0 < a + b

Assumes right covariance. The lemma assuming left covariance is Left.add_pos'.

theorem Right.one_lt_mul' {α : Type u_1} [MulOneClass α] [Preorder α] [MulRightMono α] {a : α} {b : α} (ha : 1 < a) (hb : 1 < b) :
1 < a * b

Assumes right covariance. The lemma assuming left covariance is Left.one_lt_mul'.

theorem mul_le_one' {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftMono α] {a : α} {b : α} (ha : a 1) (hb : b 1) :
a * b 1

Alias of Left.mul_le_one.


Assumes left covariance. The lemma assuming right covariance is Right.mul_le_one.

theorem mul_lt_one_of_le_of_lt {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftStrictMono α] {a : α} {b : α} (ha : a 1) (hb : b < 1) :
a * b < 1

Alias of Left.mul_lt_one_of_le_of_lt.


Assumes left covariance. The lemma assuming right covariance is Right.mul_lt_one_of_le_of_lt.

theorem mul_lt_one_of_lt_of_le {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftMono α] {a : α} {b : α} (ha : a < 1) (hb : b 1) :
a * b < 1

Alias of Left.mul_lt_one_of_lt_of_le.


Assumes left covariance. The lemma assuming right covariance is Right.mul_lt_one_of_lt_of_le.

theorem mul_lt_one {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftStrictMono α] {a : α} {b : α} (ha : a < 1) (hb : b < 1) :
a * b < 1

Alias of Left.mul_lt_one.


Assumes left covariance. The lemma assuming right covariance is Right.mul_lt_one.

theorem mul_lt_one' {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftMono α] {a : α} {b : α} (ha : a < 1) (hb : b < 1) :
a * b < 1

Alias of Left.mul_lt_one'.


Assumes left covariance. The lemma assuming right covariance is Right.mul_lt_one'.

theorem add_nonpos {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a : α} {b : α} (ha : a 0) (hb : b 0) :
a + b 0

Alias of Left.add_nonpos.

theorem add_neg_of_nonpos_of_neg {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] {a : α} {b : α} (ha : a 0) (hb : b < 0) :
a + b < 0

Alias of Left.add_neg_of_nonpos_of_neg.

theorem add_neg_of_neg_of_nonpos {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a : α} {b : α} (ha : a < 0) (hb : b 0) :
a + b < 0

Alias of Left.add_neg_of_neg_of_nonpos.

theorem add_neg {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] {a : α} {b : α} (ha : a < 0) (hb : b < 0) :
a + b < 0

Alias of Left.add_neg.

theorem add_neg' {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a : α} {b : α} (ha : a < 0) (hb : b < 0) :
a + b < 0

Alias of Left.add_neg'.

theorem one_le_mul {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftMono α] {a : α} {b : α} (ha : 1 a) (hb : 1 b) :
1 a * b

Alias of Left.one_le_mul.


Assumes left covariance. The lemma assuming right covariance is Right.one_le_mul.

theorem one_lt_mul_of_le_of_lt' {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftStrictMono α] {a : α} {b : α} (ha : 1 a) (hb : 1 < b) :
1 < a * b

Alias of Left.one_lt_mul_of_le_of_lt.


Assumes left covariance. The lemma assuming right covariance is Right.one_lt_mul_of_le_of_lt.

theorem one_lt_mul_of_lt_of_le' {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftMono α] {a : α} {b : α} (ha : 1 < a) (hb : 1 b) :
1 < a * b

Alias of Left.one_lt_mul_of_lt_of_le.


Assumes left covariance. The lemma assuming right covariance is Right.one_lt_mul_of_lt_of_le.

theorem one_lt_mul' {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftStrictMono α] {a : α} {b : α} (ha : 1 < a) (hb : 1 < b) :
1 < a * b

Alias of Left.one_lt_mul.


Assumes left covariance. The lemma assuming right covariance is Right.one_lt_mul.

theorem one_lt_mul'' {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftMono α] {a : α} {b : α} (ha : 1 < a) (hb : 1 < b) :
1 < a * b

Alias of Left.one_lt_mul'.


Assumes left covariance. The lemma assuming right covariance is Right.one_lt_mul'.

theorem add_nonneg {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a : α} {b : α} (ha : 0 a) (hb : 0 b) :
0 a + b

Alias of Left.add_nonneg.

theorem add_pos_of_nonneg_of_pos {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] {a : α} {b : α} (ha : 0 a) (hb : 0 < b) :
0 < a + b

Alias of Left.add_pos_of_nonneg_of_pos.

theorem add_pos_of_pos_of_nonneg {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a : α} {b : α} (ha : 0 < a) (hb : 0 b) :
0 < a + b

Alias of Left.add_pos_of_pos_of_nonneg.

theorem add_pos {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftStrictMono α] {a : α} {b : α} (ha : 0 < a) (hb : 0 < b) :
0 < a + b

Alias of Left.add_pos.

theorem add_pos' {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a : α} {b : α} (ha : 0 < a) (hb : 0 < b) :
0 < a + b

Alias of Left.add_pos'.

theorem lt_of_add_lt_of_nonneg_left {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a : α} {b : α} {c : α} (h : a + b < c) (hle : 0 b) :
a < c
theorem lt_of_mul_lt_of_one_le_left {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftMono α] {a : α} {b : α} {c : α} (h : a * b < c) (hle : 1 b) :
a < c
theorem le_of_add_le_of_nonneg_left {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a : α} {b : α} {c : α} (h : a + b c) (hle : 0 b) :
a c
theorem le_of_mul_le_of_one_le_left {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftMono α] {a : α} {b : α} {c : α} (h : a * b c) (hle : 1 b) :
a c
theorem lt_of_lt_add_of_nonpos_left {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a : α} {b : α} {c : α} (h : a < b + c) (hle : c 0) :
a < b
theorem lt_of_lt_mul_of_le_one_left {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftMono α] {a : α} {b : α} {c : α} (h : a < b * c) (hle : c 1) :
a < b
theorem le_of_le_add_of_nonpos_left {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {a : α} {b : α} {c : α} (h : a b + c) (hle : c 0) :
a b
theorem le_of_le_mul_of_le_one_left {α : Type u_1} [MulOneClass α] [Preorder α] [MulLeftMono α] {a : α} {b : α} {c : α} (h : a b * c) (hle : c 1) :
a b
theorem lt_of_add_lt_of_nonneg_right {α : Type u_1} [AddZeroClass α] [Preorder α] [AddRightMono α] {a : α} {b : α} {c : α} (h : a + b < c) (hle : 0 a) :
b < c
theorem lt_of_mul_lt_of_one_le_right {α : Type u_1} [MulOneClass α] [Preorder α] [MulRightMono α] {a : α} {b : α} {c : α} (h : a * b < c) (hle : 1 a) :
b < c
theorem le_of_add_le_of_nonneg_right {α : Type u_1} [AddZeroClass α] [Preorder α] [AddRightMono α] {a : α} {b : α} {c : α} (h : a + b c) (hle : 0 a) :
b c
theorem le_of_mul_le_of_one_le_right {α : Type u_1} [MulOneClass α] [Preorder α] [MulRightMono α] {a : α} {b : α} {c : α} (h : a * b c) (hle : 1 a) :
b c
theorem lt_of_lt_add_of_nonpos_right {α : Type u_1} [AddZeroClass α] [Preorder α] [AddRightMono α] {a : α} {b : α} {c : α} (h : a < b + c) (hle : b 0) :
a < c
theorem lt_of_lt_mul_of_le_one_right {α : Type u_1} [MulOneClass α] [Preorder α] [MulRightMono α] {a : α} {b : α} {c : α} (h : a < b * c) (hle : b 1) :
a < c
theorem le_of_le_add_of_nonpos_right {α : Type u_1} [AddZeroClass α] [Preorder α] [AddRightMono α] {a : α} {b : α} {c : α} (h : a b + c) (hle : b 0) :
a c
theorem le_of_le_mul_of_le_one_right {α : Type u_1} [MulOneClass α] [Preorder α] [MulRightMono α] {a : α} {b : α} {c : α} (h : a b * c) (hle : b 1) :
a c
theorem add_eq_zero_iff_of_nonneg {α : Type u_1} [AddZeroClass α] [PartialOrder α] [AddLeftMono α] [AddRightMono α] {a : α} {b : α} (ha : 0 a) (hb : 0 b) :
a + b = 0 a = 0 b = 0
theorem mul_eq_one_iff_of_one_le {α : Type u_1} [MulOneClass α] [PartialOrder α] [MulLeftMono α] [MulRightMono α] {a : α} {b : α} (ha : 1 a) (hb : 1 b) :
a * b = 1 a = 1 b = 1
@[deprecated mul_eq_one_iff_of_one_le]
theorem mul_eq_one_iff' {α : Type u_1} [MulOneClass α] [PartialOrder α] [MulLeftMono α] [MulRightMono α] {a : α} {b : α} (ha : 1 a) (hb : 1 b) :
a * b = 1 a = 1 b = 1

Alias of mul_eq_one_iff_of_one_le.

@[deprecated add_eq_zero_iff_of_nonneg]
theorem add_eq_zero_iff' {α : Type u_1} [AddZeroClass α] [PartialOrder α] [AddLeftMono α] [AddRightMono α] {a : α} {b : α} (ha : 0 a) (hb : 0 b) :
a + b = 0 a = 0 b = 0

Alias of add_eq_zero_iff_of_nonneg.

theorem eq_zero_of_add_nonneg_left {α : Type u_1} [AddZeroClass α] [PartialOrder α] [AddLeftMono α] {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} [MulOneClass α] [PartialOrder α] [MulLeftMono α] {a : α} {b : α} (ha : a 1) (hb : b 1) (hab : 1 a * b) :
a = 1
theorem eq_zero_of_add_nonpos_left {α : Type u_1} [AddZeroClass α] [PartialOrder α] [AddLeftMono α] {a : α} {b : α} (ha : 0 a) (hb : 0 b) (hab : a + b 0) :
a = 0
theorem eq_one_of_mul_le_one_left {α : Type u_1} [MulOneClass α] [PartialOrder α] [MulLeftMono α] {a : α} {b : α} (ha : 1 a) (hb : 1 b) (hab : a * b 1) :
a = 1
theorem eq_zero_of_add_nonneg_right {α : Type u_1} [AddZeroClass α] [PartialOrder α] [AddRightMono α] {a : α} {b : α} (ha : a 0) (hb : b 0) (hab : 0 a + b) :
b = 0
theorem eq_one_of_one_le_mul_right {α : Type u_1} [MulOneClass α] [PartialOrder α] [MulRightMono α] {a : α} {b : α} (ha : a 1) (hb : b 1) (hab : 1 a * b) :
b = 1
theorem eq_zero_of_add_nonpos_right {α : Type u_1} [AddZeroClass α] [PartialOrder α] [AddRightMono α] {a : α} {b : α} (ha : 0 a) (hb : 0 b) (hab : a + b 0) :
b = 0
theorem eq_one_of_mul_le_one_right {α : Type u_1} [MulOneClass α] [PartialOrder α] [MulRightMono α] {a : α} {b : α} (ha : 1 a) (hb : 1 b) (hab : a * b 1) :
b = 1
theorem exists_square_le {α : Type u_1} [MulOneClass α] [LinearOrder α] [MulLeftStrictMono α] (a : α) :
∃ (b : α), b * b a

An additive semigroup with a partial order and satisfying AddLeftCancelSemigroup (i.e. c + a < c + b → a < b) is a AddLeftCancelSemigroup.

Equations
Instances For

    A semigroup with a partial order and satisfying LeftCancelSemigroup (i.e. a * c < b * c → a < b) is a LeftCancelSemigroup.

    Equations
    Instances For

      An additive semigroup with a partial order and satisfying AddRightCancelSemigroup (a + c < b + c → a < b) is a AddRightCancelSemigroup.

      Equations
      Instances For

        A semigroup with a partial order and satisfying RightCancelSemigroup (i.e. a * c < b * c → a < b) is a RightCancelSemigroup.

        Equations
        Instances For
          theorem Monotone.const_add {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} [AddLeftMono α] (hf : Monotone f) (a : α) :
          Monotone fun (x : β) => a + f x
          theorem Monotone.const_mul' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} [MulLeftMono α] (hf : Monotone f) (a : α) :
          Monotone fun (x : β) => a * f x
          theorem MonotoneOn.const_add {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} {s : Set β} [AddLeftMono α] (hf : MonotoneOn f s) (a : α) :
          MonotoneOn (fun (x : β) => a + f x) s
          theorem MonotoneOn.const_mul' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} {s : Set β} [MulLeftMono α] (hf : MonotoneOn f s) (a : α) :
          MonotoneOn (fun (x : β) => a * f x) s
          theorem Antitone.const_add {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} [AddLeftMono α] (hf : Antitone f) (a : α) :
          Antitone fun (x : β) => a + f x
          theorem Antitone.const_mul' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} [MulLeftMono α] (hf : Antitone f) (a : α) :
          Antitone fun (x : β) => a * f x
          theorem AntitoneOn.const_add {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} {s : Set β} [AddLeftMono α] (hf : AntitoneOn f s) (a : α) :
          AntitoneOn (fun (x : β) => a + f x) s
          theorem AntitoneOn.const_mul' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} {s : Set β} [MulLeftMono α] (hf : AntitoneOn f s) (a : α) :
          AntitoneOn (fun (x : β) => a * f x) s
          theorem Monotone.add_const {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} [AddRightMono α] (hf : Monotone f) (a : α) :
          Monotone fun (x : β) => f x + a
          theorem Monotone.mul_const' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} [MulRightMono α] (hf : Monotone f) (a : α) :
          Monotone fun (x : β) => f x * a
          theorem MonotoneOn.add_const {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} {s : Set β} [AddRightMono α] (hf : MonotoneOn f s) (a : α) :
          MonotoneOn (fun (x : β) => f x + a) s
          theorem MonotoneOn.mul_const' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} {s : Set β} [MulRightMono α] (hf : MonotoneOn f s) (a : α) :
          MonotoneOn (fun (x : β) => f x * a) s
          theorem Antitone.add_const {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} [AddRightMono α] (hf : Antitone f) (a : α) :
          Antitone fun (x : β) => f x + a
          theorem Antitone.mul_const' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} [MulRightMono α] (hf : Antitone f) (a : α) :
          Antitone fun (x : β) => f x * a
          theorem AntitoneOn.add_const {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} {s : Set β} [AddRightMono α] (hf : AntitoneOn f s) (a : α) :
          AntitoneOn (fun (x : β) => f x + a) s
          theorem AntitoneOn.mul_const' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} {s : Set β} [MulRightMono α] (hf : AntitoneOn f s) (a : α) :
          AntitoneOn (fun (x : β) => f x * a) s
          theorem Monotone.add {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} {g : βα} [AddLeftMono α] [AddRightMono α] (hf : Monotone f) (hg : Monotone g) :
          Monotone fun (x : β) => f x + g x

          The sum of two monotone functions is monotone.

          theorem Monotone.mul' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} {g : βα} [MulLeftMono α] [MulRightMono α] (hf : Monotone f) (hg : Monotone g) :
          Monotone fun (x : β) => f x * g x

          The product of two monotone functions is monotone.

          theorem MonotoneOn.add {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} {g : βα} {s : Set β} [AddLeftMono α] [AddRightMono α] (hf : MonotoneOn f s) (hg : MonotoneOn g s) :
          MonotoneOn (fun (x : β) => f x + g x) s

          The sum of two monotone functions is monotone.

          theorem MonotoneOn.mul' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} {g : βα} {s : Set β} [MulLeftMono α] [MulRightMono α] (hf : MonotoneOn f s) (hg : MonotoneOn g s) :
          MonotoneOn (fun (x : β) => f x * g x) s

          The product of two monotone functions is monotone.

          theorem Antitone.add {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} {g : βα} [AddLeftMono α] [AddRightMono α] (hf : Antitone f) (hg : Antitone g) :
          Antitone fun (x : β) => f x + g x

          The sum of two antitone functions is antitone.

          theorem Antitone.mul' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} {g : βα} [MulLeftMono α] [MulRightMono α] (hf : Antitone f) (hg : Antitone g) :
          Antitone fun (x : β) => f x * g x

          The product of two antitone functions is antitone.

          theorem AntitoneOn.add {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} {g : βα} {s : Set β} [AddLeftMono α] [AddRightMono α] (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
          AntitoneOn (fun (x : β) => f x + g x) s

          The sum of two antitone functions is antitone.

          theorem AntitoneOn.mul' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} {g : βα} {s : Set β} [MulLeftMono α] [MulRightMono α] (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
          AntitoneOn (fun (x : β) => f x * g x) s

          The product of two antitone functions is antitone.

          theorem StrictMono.const_add {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} [AddLeftStrictMono α] (hf : StrictMono f) (c : α) :
          StrictMono fun (x : β) => c + f x
          theorem StrictMono.const_mul' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} [MulLeftStrictMono α] (hf : StrictMono f) (c : α) :
          StrictMono fun (x : β) => c * f x
          theorem StrictMonoOn.const_add {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} {s : Set β} [AddLeftStrictMono α] (hf : StrictMonoOn f s) (c : α) :
          StrictMonoOn (fun (x : β) => c + f x) s
          theorem StrictMonoOn.const_mul' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} {s : Set β} [MulLeftStrictMono α] (hf : StrictMonoOn f s) (c : α) :
          StrictMonoOn (fun (x : β) => c * f x) s
          theorem StrictAnti.const_add {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} [AddLeftStrictMono α] (hf : StrictAnti f) (c : α) :
          StrictAnti fun (x : β) => c + f x
          theorem StrictAnti.const_mul' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} [MulLeftStrictMono α] (hf : StrictAnti f) (c : α) :
          StrictAnti fun (x : β) => c * f x
          theorem StrictAntiOn.const_add {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} {s : Set β} [AddLeftStrictMono α] (hf : StrictAntiOn f s) (c : α) :
          StrictAntiOn (fun (x : β) => c + f x) s
          theorem StrictAntiOn.const_mul' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} {s : Set β} [MulLeftStrictMono α] (hf : StrictAntiOn f s) (c : α) :
          StrictAntiOn (fun (x : β) => c * f x) s
          theorem StrictMono.add_const {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} [AddRightStrictMono α] (hf : StrictMono f) (c : α) :
          StrictMono fun (x : β) => f x + c
          theorem StrictMono.mul_const' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} [MulRightStrictMono α] (hf : StrictMono f) (c : α) :
          StrictMono fun (x : β) => f x * c
          theorem StrictMonoOn.add_const {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} {s : Set β} [AddRightStrictMono α] (hf : StrictMonoOn f s) (c : α) :
          StrictMonoOn (fun (x : β) => f x + c) s
          theorem StrictMonoOn.mul_const' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} {s : Set β} [MulRightStrictMono α] (hf : StrictMonoOn f s) (c : α) :
          StrictMonoOn (fun (x : β) => f x * c) s
          theorem StrictAnti.add_const {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} [AddRightStrictMono α] (hf : StrictAnti f) (c : α) :
          StrictAnti fun (x : β) => f x + c
          theorem StrictAnti.mul_const' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} [MulRightStrictMono α] (hf : StrictAnti f) (c : α) :
          StrictAnti fun (x : β) => f x * c
          theorem StrictAntiOn.add_const {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} {s : Set β} [AddRightStrictMono α] (hf : StrictAntiOn f s) (c : α) :
          StrictAntiOn (fun (x : β) => f x + c) s
          theorem StrictAntiOn.mul_const' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} {s : Set β} [MulRightStrictMono α] (hf : StrictAntiOn f s) (c : α) :
          StrictAntiOn (fun (x : β) => f x * c) s
          theorem StrictMono.add {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} {g : βα} [AddLeftStrictMono α] [AddRightStrictMono α] (hf : StrictMono f) (hg : StrictMono g) :
          StrictMono fun (x : β) => f x + g x

          The sum of two strictly monotone functions is strictly monotone.

          theorem StrictMono.mul' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} {g : βα} [MulLeftStrictMono α] [MulRightStrictMono α] (hf : StrictMono f) (hg : StrictMono g) :
          StrictMono fun (x : β) => f x * g x

          The product of two strictly monotone functions is strictly monotone.

          theorem StrictMonoOn.add {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} {g : βα} {s : Set β} [AddLeftStrictMono α] [AddRightStrictMono α] (hf : StrictMonoOn f s) (hg : StrictMonoOn g s) :
          StrictMonoOn (fun (x : β) => f x + g x) s

          The sum of two strictly monotone functions is strictly monotone.

          theorem StrictMonoOn.mul' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} {g : βα} {s : Set β} [MulLeftStrictMono α] [MulRightStrictMono α] (hf : StrictMonoOn f s) (hg : StrictMonoOn g s) :
          StrictMonoOn (fun (x : β) => f x * g x) s

          The product of two strictly monotone functions is strictly monotone.

          theorem StrictAnti.add {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} {g : βα} [AddLeftStrictMono α] [AddRightStrictMono α] (hf : StrictAnti f) (hg : StrictAnti g) :
          StrictAnti fun (x : β) => f x + g x

          The sum of two strictly antitone functions is strictly antitone.

          theorem StrictAnti.mul' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} {g : βα} [MulLeftStrictMono α] [MulRightStrictMono α] (hf : StrictAnti f) (hg : StrictAnti g) :
          StrictAnti fun (x : β) => f x * g x

          The product of two strictly antitone functions is strictly antitone.

          theorem StrictAntiOn.add {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} {g : βα} {s : Set β} [AddLeftStrictMono α] [AddRightStrictMono α] (hf : StrictAntiOn f s) (hg : StrictAntiOn g s) :
          StrictAntiOn (fun (x : β) => f x + g x) s

          The sum of two strictly antitone functions is strictly antitone.

          theorem StrictAntiOn.mul' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} {g : βα} {s : Set β} [MulLeftStrictMono α] [MulRightStrictMono α] (hf : StrictAntiOn f s) (hg : StrictAntiOn g s) :
          StrictAntiOn (fun (x : β) => f x * g x) s

          The product of two strictly antitone functions is strictly antitone.

          theorem Monotone.add_strictMono {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] [AddLeftStrictMono α] [AddRightMono α] {f : βα} {g : βα} (hf : Monotone f) (hg : StrictMono g) :
          StrictMono fun (x : β) => f x + g x

          The sum of a monotone function and a strictly monotone function is strictly monotone.

          theorem Monotone.mul_strictMono' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] [MulLeftStrictMono α] [MulRightMono α] {f : βα} {g : βα} (hf : Monotone f) (hg : StrictMono g) :
          StrictMono fun (x : β) => f x * g x

          The product of a monotone function and a strictly monotone function is strictly monotone.

          theorem MonotoneOn.add_strictMono {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {s : Set β} [AddLeftStrictMono α] [AddRightMono α] {f : βα} {g : βα} (hf : MonotoneOn f s) (hg : StrictMonoOn g s) :
          StrictMonoOn (fun (x : β) => f x + g x) s

          The sum of a monotone function and a strictly monotone function is strictly monotone.

          theorem MonotoneOn.mul_strictMono' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {s : Set β} [MulLeftStrictMono α] [MulRightMono α] {f : βα} {g : βα} (hf : MonotoneOn f s) (hg : StrictMonoOn g s) :
          StrictMonoOn (fun (x : β) => f x * g x) s

          The product of a monotone function and a strictly monotone function is strictly monotone.

          theorem Antitone.add_strictAnti {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] [AddLeftStrictMono α] [AddRightMono α] {f : βα} {g : βα} (hf : Antitone f) (hg : StrictAnti g) :
          StrictAnti fun (x : β) => f x + g x

          The sum of an antitone function and a strictly antitone function is strictly antitone.

          theorem Antitone.mul_strictAnti' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] [MulLeftStrictMono α] [MulRightMono α] {f : βα} {g : βα} (hf : Antitone f) (hg : StrictAnti g) :
          StrictAnti fun (x : β) => f x * g x

          The product of an antitone function and a strictly antitone function is strictly antitone.

          theorem AntitoneOn.add_strictAnti {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {s : Set β} [AddLeftStrictMono α] [AddRightMono α] {f : βα} {g : βα} (hf : AntitoneOn f s) (hg : StrictAntiOn g s) :
          StrictAntiOn (fun (x : β) => f x + g x) s

          The sum of an antitone function and a strictly antitone function is strictly antitone.

          theorem AntitoneOn.mul_strictAnti' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {s : Set β} [MulLeftStrictMono α] [MulRightMono α] {f : βα} {g : βα} (hf : AntitoneOn f s) (hg : StrictAntiOn g s) :
          StrictAntiOn (fun (x : β) => f x * g x) s

          The product of an antitone function and a strictly antitone function is strictly antitone.

          theorem StrictMono.add_monotone {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} {g : βα} [AddLeftMono α] [AddRightStrictMono α] (hf : StrictMono f) (hg : Monotone g) :
          StrictMono fun (x : β) => f x + g x

          The sum of a strictly monotone function and a monotone function is strictly monotone.

          theorem StrictMono.mul_monotone' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} {g : βα} [MulLeftMono α] [MulRightStrictMono α] (hf : StrictMono f) (hg : Monotone g) :
          StrictMono fun (x : β) => f x * g x

          The product of a strictly monotone function and a monotone function is strictly monotone.

          theorem StrictMonoOn.add_monotone {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} {g : βα} {s : Set β} [AddLeftMono α] [AddRightStrictMono α] (hf : StrictMonoOn f s) (hg : MonotoneOn g s) :
          StrictMonoOn (fun (x : β) => f x + g x) s

          The sum of a strictly monotone function and a monotone function is strictly monotone.

          theorem StrictMonoOn.mul_monotone' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} {g : βα} {s : Set β} [MulLeftMono α] [MulRightStrictMono α] (hf : StrictMonoOn f s) (hg : MonotoneOn g s) :
          StrictMonoOn (fun (x : β) => f x * g x) s

          The product of a strictly monotone function and a monotone function is strictly monotone.

          theorem StrictAnti.add_antitone {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} {g : βα} [AddLeftMono α] [AddRightStrictMono α] (hf : StrictAnti f) (hg : Antitone g) :
          StrictAnti fun (x : β) => f x + g x

          The sum of a strictly antitone function and an antitone function is strictly antitone.

          theorem StrictAnti.mul_antitone' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} {g : βα} [MulLeftMono α] [MulRightStrictMono α] (hf : StrictAnti f) (hg : Antitone g) :
          StrictAnti fun (x : β) => f x * g x

          The product of a strictly antitone function and an antitone function is strictly antitone.

          theorem StrictAntiOn.add_antitone {α : Type u_1} {β : Type u_2} [Add α] [Preorder α] [Preorder β] {f : βα} {g : βα} {s : Set β} [AddLeftMono α] [AddRightStrictMono α] (hf : StrictAntiOn f s) (hg : AntitoneOn g s) :
          StrictAntiOn (fun (x : β) => f x + g x) s

          The sum of a strictly antitone function and an antitone function is strictly antitone.

          theorem StrictAntiOn.mul_antitone' {α : Type u_1} {β : Type u_2} [Mul α] [Preorder α] [Preorder β] {f : βα} {g : βα} {s : Set β} [MulLeftMono α] [MulRightStrictMono α] (hf : StrictAntiOn f s) (hg : AntitoneOn g s) :
          StrictAntiOn (fun (x : β) => f x * g x) s

          The product of a strictly antitone function and an antitone function is strictly antitone.

          @[simp]
          theorem cmp_add_left {α : Type u_3} [Add α] [LinearOrder α] [AddLeftStrictMono α] (a : α) (b : α) (c : α) :
          cmp (a + b) (a + c) = cmp b c
          @[simp]
          theorem cmp_mul_left' {α : Type u_3} [Mul α] [LinearOrder α] [MulLeftStrictMono α] (a : α) (b : α) (c : α) :
          cmp (a * b) (a * c) = cmp b c
          @[simp]
          theorem cmp_add_right {α : Type u_3} [Add α] [LinearOrder α] [AddRightStrictMono α] (a : α) (b : α) (c : α) :
          cmp (a + c) (b + c) = cmp a b
          @[simp]
          theorem cmp_mul_right' {α : Type u_3} [Mul α] [LinearOrder α] [MulRightStrictMono α] (a : α) (b : α) (c : α) :
          cmp (a * c) (b * c) = cmp a b
          def AddLECancellable {α : Type u_1} [Add α] [LE α] (a : α) :

          An element a : α is AddLECancellable if x ↦ a + x is order-reflecting. We will make a separate version of many lemmas that require [MulLeftReflectLE α] with AddLECancellable assumptions instead. These lemmas can then be instantiated to specific types, like ENNReal, where we can replace the assumption AddLECancellable x by x ≠ ∞.

          Equations
          Instances For
            def MulLECancellable {α : Type u_1} [Mul α] [LE α] (a : α) :

            An element a : α is MulLECancellable if x ↦ a * x is order-reflecting. We will make a separate version of many lemmas that require [MulLeftReflectLE α] with MulLECancellable assumptions instead. These lemmas can then be instantiated to specific types, like ENNReal, where we can replace the assumption AddLECancellable x by x ≠ ∞.

            Equations
            Instances For
              @[simp]
              theorem addLECancellable_zero {α : Type u_1} [AddMonoid α] [LE α] :
              @[simp]
              theorem mulLECancellable_one {α : Type u_1} [Monoid α] [LE α] :
              theorem AddLECancellable.Injective {α : Type u_1} [Add α] [PartialOrder α] {a : α} (ha : AddLECancellable a) :
              Function.Injective fun (x : α) => a + x
              theorem MulLECancellable.Injective {α : Type u_1} [Mul α] [PartialOrder α] {a : α} (ha : MulLECancellable a) :
              Function.Injective fun (x : α) => a * x
              theorem AddLECancellable.inj {α : Type u_1} [Add α] [PartialOrder α] {a : α} {b : α} {c : α} (ha : AddLECancellable a) :
              a + b = a + c b = c
              theorem MulLECancellable.inj {α : Type u_1} [Mul α] [PartialOrder α] {a : α} {b : α} {c : α} (ha : MulLECancellable a) :
              a * b = a * c b = c
              theorem AddLECancellable.injective_left {α : Type u_1} [Add α] [i : Std.Commutative fun (x1 x2 : α) => x1 + x2] [PartialOrder α] {a : α} (ha : AddLECancellable a) :
              Function.Injective fun (x : α) => x + a
              theorem MulLECancellable.injective_left {α : Type u_1} [Mul α] [i : Std.Commutative fun (x1 x2 : α) => x1 * x2] [PartialOrder α] {a : α} (ha : MulLECancellable a) :
              Function.Injective fun (x : α) => x * a
              theorem AddLECancellable.inj_left {α : Type u_1} [Add α] [Std.Commutative fun (x1 x2 : α) => x1 + x2] [PartialOrder α] {a : α} {b : α} {c : α} (hc : AddLECancellable c) :
              a + c = b + c a = b
              theorem MulLECancellable.inj_left {α : Type u_1} [Mul α] [Std.Commutative fun (x1 x2 : α) => x1 * x2] [PartialOrder α] {a : α} {b : α} {c : α} (hc : MulLECancellable c) :
              a * c = b * c a = b
              theorem AddLECancellable.add_le_add_iff_left {α : Type u_1} [LE α] [Add α] [AddLeftMono α] {a : α} {b : α} {c : α} (ha : AddLECancellable a) :
              a + b a + c b c
              theorem MulLECancellable.mul_le_mul_iff_left {α : Type u_1} [LE α] [Mul α] [MulLeftMono α] {a : α} {b : α} {c : α} (ha : MulLECancellable a) :
              a * b a * c b c
              theorem AddLECancellable.add_le_add_iff_right {α : Type u_1} [LE α] [Add α] [i : Std.Commutative fun (x1 x2 : α) => x1 + x2] [AddLeftMono α] {a : α} {b : α} {c : α} (ha : AddLECancellable a) :
              b + a c + a b c
              theorem MulLECancellable.mul_le_mul_iff_right {α : Type u_1} [LE α] [Mul α] [i : Std.Commutative fun (x1 x2 : α) => x1 * x2] [MulLeftMono α] {a : α} {b : α} {c : α} (ha : MulLECancellable a) :
              b * a c * a b c
              theorem AddLECancellable.le_add_iff_nonneg_right {α : Type u_1} [LE α] [AddZeroClass α] [AddLeftMono α] {a : α} {b : α} (ha : AddLECancellable a) :
              a a + b 0 b
              theorem MulLECancellable.le_mul_iff_one_le_right {α : Type u_1} [LE α] [MulOneClass α] [MulLeftMono α] {a : α} {b : α} (ha : MulLECancellable a) :
              a a * b 1 b
              theorem AddLECancellable.add_le_iff_nonpos_right {α : Type u_1} [LE α] [AddZeroClass α] [AddLeftMono α] {a : α} {b : α} (ha : AddLECancellable a) :
              a + b a b 0
              theorem MulLECancellable.mul_le_iff_le_one_right {α : Type u_1} [LE α] [MulOneClass α] [MulLeftMono α] {a : α} {b : α} (ha : MulLECancellable a) :
              a * b a b 1
              theorem AddLECancellable.le_add_iff_nonneg_left {α : Type u_1} [LE α] [AddZeroClass α] [i : Std.Commutative fun (x1 x2 : α) => x1 + x2] [AddLeftMono α] {a : α} {b : α} (ha : AddLECancellable a) :
              a b + a 0 b
              theorem MulLECancellable.le_mul_iff_one_le_left {α : Type u_1} [LE α] [MulOneClass α] [i : Std.Commutative fun (x1 x2 : α) => x1 * x2] [MulLeftMono α] {a : α} {b : α} (ha : MulLECancellable a) :
              a b * a 1 b
              theorem AddLECancellable.add_le_iff_nonpos_left {α : Type u_1} [LE α] [AddZeroClass α] [i : Std.Commutative fun (x1 x2 : α) => x1 + x2] [AddLeftMono α] {a : α} {b : α} (ha : AddLECancellable a) :
              b + a a b 0
              theorem MulLECancellable.mul_le_iff_le_one_left {α : Type u_1} [LE α] [MulOneClass α] [i : Std.Commutative fun (x1 x2 : α) => x1 * x2] [MulLeftMono α] {a : α} {b : α} (ha : MulLECancellable a) :
              b * a a b 1
              theorem AddLECancellable.add {α : Type u_1} [LE α] [AddSemigroup α] {a : α} {b : α} (ha : AddLECancellable a) (hb : AddLECancellable b) :
              theorem MulLECancellable.mul {α : Type u_1} [LE α] [Semigroup α] {a : α} {b : α} (ha : MulLECancellable a) (hb : MulLECancellable b) :
              theorem AddLECancellable.of_add_right {α : Type u_1} [LE α] [AddSemigroup α] [AddLeftMono α] {a : α} {b : α} (h : AddLECancellable (a + b)) :
              theorem MulLECancellable.of_mul_right {α : Type u_1} [LE α] [Semigroup α] [MulLeftMono α] {a : α} {b : α} (h : MulLECancellable (a * b)) :
              theorem AddLECancellable.of_add_left {α : Type u_1} [LE α] [AddCommSemigroup α] [AddLeftMono α] {a : α} {b : α} (h : AddLECancellable (a + b)) :
              theorem MulLECancellable.of_mul_left {α : Type u_1} [LE α] [CommSemigroup α] [MulLeftMono α] {a : α} {b : α} (h : MulLECancellable (a * b)) :
              @[simp]
              theorem addLECancellable_add {α : Type u_1} [LE α] [AddCommSemigroup α] [AddLeftMono α] {a : α} {b : α} :
              @[simp]
              theorem mulLECancellable_mul {α : Type u_1} [LE α] [CommSemigroup α] [MulLeftMono α] {a : α} {b : α} :