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.

instance Nat.instMulLeftMono : MulLeftMono ℕ

Equations

• Nat.instMulLeftMono = ⋯

instance Int.instAddLeftMono : AddLeftMono ℤ

Equations

• Int.instAddLeftMono = ⋯

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

def Contravariant.toAddLeftCancelSemigroup {α : Type u_1} [AddSemigroup α] [PartialOrder α] [AddLeftReflectLE α] : AddLeftCancelSemigroup α

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

Equations

• Contravariant.toAddLeftCancelSemigroup = AddLeftCancelSemigroup.mk ⋯

theorem Contravariant.toAddLeftCancelSemigroup.proof_1 {α : Type u_1} [AddSemigroup α] [PartialOrder α] [AddLeftReflectLE α] : ∀ (x x_1 x_2 : α), x + x_1 = x + x_2 → x_1 = x_2

def Contravariant.toLeftCancelSemigroup {α : Type u_1} [Semigroup α] [PartialOrder α] [MulLeftReflectLE α] : LeftCancelSemigroup α

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

Equations

• Contravariant.toLeftCancelSemigroup = LeftCancelSemigroup.mk ⋯

def Contravariant.toAddRightCancelSemigroup {α : Type u_1} [AddSemigroup α] [PartialOrder α] [AddRightReflectLE α] : AddRightCancelSemigroup α

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

Equations

• Contravariant.toAddRightCancelSemigroup = AddRightCancelSemigroup.mk ⋯

theorem Contravariant.toAddRightCancelSemigroup.proof_1 {α : Type u_1} [AddSemigroup α] [PartialOrder α] [AddRightReflectLE α] : ∀ (x x_1 x_2 : α), x + x_1 = x_2 + x_1 → x = x_2

def Contravariant.toRightCancelSemigroup {α : Type u_1} [Semigroup α] [PartialOrder α] [MulRightReflectLE α] : RightCancelSemigroup α

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

Equations

• Contravariant.toRightCancelSemigroup = RightCancelSemigroup.mk ⋯

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 : α) : Prop

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

• AddLECancellable a = ∀ ⦃b c : α⦄, a + b ≤ a + c → b ≤ c

def MulLECancellable {α : Type u_1} [Mul α] [LE α] (a : α) : Prop

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

• MulLECancellable a = ∀ ⦃b c : α⦄, a * b ≤ a * c → b ≤ c

theorem Contravariant.AddLECancellable {α : Type u_1} [Add α] [LE α] [AddLeftReflectLE α] {a : α} : AddLECancellable a

theorem Contravariant.MulLECancellable {α : Type u_1} [Mul α] [LE α] [MulLeftReflectLE α] {a : α} : MulLECancellable a

@[simp]

theorem addLECancellable_zero {α : Type u_1} [AddMonoid α] [LE α] : AddLECancellable 0

@[simp]

theorem mulLECancellable_one {α : Type u_1} [Monoid α] [LE α] : MulLECancellable 1

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) : AddLECancellable (a + b)

theorem MulLECancellable.mul {α : Type u_1} [LE α] [Semigroup α] {a : α} {b : α} (ha : MulLECancellable a) (hb : MulLECancellable b) : MulLECancellable (a * b)

theorem AddLECancellable.of_add_right {α : Type u_1} [LE α] [AddSemigroup α] [AddLeftMono α] {a : α} {b : α} (h : AddLECancellable (a + b)) : AddLECancellable b

theorem MulLECancellable.of_mul_right {α : Type u_1} [LE α] [Semigroup α] [MulLeftMono α] {a : α} {b : α} (h : MulLECancellable (a * b)) : MulLECancellable b

theorem AddLECancellable.of_add_left {α : Type u_1} [LE α] [AddCommSemigroup α] [AddLeftMono α] {a : α} {b : α} (h : AddLECancellable (a + b)) : AddLECancellable a

theorem MulLECancellable.of_mul_left {α : Type u_1} [LE α] [CommSemigroup α] [MulLeftMono α] {a : α} {b : α} (h : MulLECancellable (a * b)) : MulLECancellable a

@[simp]

theorem addLECancellable_add {α : Type u_1} [LE α] [AddCommSemigroup α] [AddLeftMono α] {a : α} {b : α} : AddLECancellable (a + b) ↔ AddLECancellable a ∧ AddLECancellable b

@[simp]

theorem mulLECancellable_mul {α : Type u_1} [LE α] [CommSemigroup α] [MulLeftMono α] {a : α} {b : α} : MulLECancellable (a * b) ↔ MulLECancellable a ∧ MulLECancellable b