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.

ink

theorem add_le_add_left {α : Type u_1} [inst : Add α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {b : α} {c : α} (bc : b ≤ c) (a : α) : a + b ≤ a + c

ink

theorem mul_le_mul_left' {α : Type u_1} [inst : Mul α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {b : α} {c : α} (bc : b ≤ c) (a : α) : a * b ≤ a * c

ink

theorem le_of_add_le_add_left {α : Type u_1} [inst : Add α] [inst : LE α] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (bc : a + b ≤ a + c) : b ≤ c

ink

theorem le_of_mul_le_mul_left' {α : Type u_1} [inst : Mul α] [inst : LE α] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (bc : a * b ≤ a * c) : b ≤ c

ink

theorem add_le_add_right {α : Type u_1} [inst : Add α] [inst : LE α] [i : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {b : α} {c : α} (bc : b ≤ c) (a : α) : b + a ≤ c + a

ink

theorem mul_le_mul_right' {α : Type u_1} [inst : Mul α] [inst : LE α] [i : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {b : α} {c : α} (bc : b ≤ c) (a : α) : b * a ≤ c * a

ink

theorem le_of_add_le_add_right {α : Type u_1} [inst : Add α] [inst : LE α] [i : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (bc : b + a ≤ c + a) : b ≤ c

ink

theorem le_of_mul_le_mul_right' {α : Type u_1} [inst : Mul α] [inst : LE α] [i : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (bc : b * a ≤ c * a) : b ≤ c

ink

@[simp]

theorem add_le_add_iff_left {α : Type u_1} [inst : Add α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) {b : α} {c : α} : a + b ≤ a + c ↔ b ≤ c

ink

@[simp]

theorem mul_le_mul_iff_left {α : Type u_1} [inst : Mul α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (a : α) {b : α} {c : α} : a * b ≤ a * c ↔ b ≤ c

ink

@[simp]

theorem add_le_add_iff_right {α : Type u_1} [inst : Add α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) {b : α} {c : α} : b + a ≤ c + a ↔ b ≤ c

ink

@[simp]

theorem mul_le_mul_iff_right {α : Type u_1} [inst : Mul α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (a : α) {b : α} {c : α} : b * a ≤ c * a ↔ b ≤ c

ink

@[simp]

theorem add_lt_add_iff_left {α : Type u_1} [inst : Add α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b : α} {c : α} : a + b < a + c ↔ b < c

ink

@[simp]

theorem mul_lt_mul_iff_left {α : Type u_1} [inst : Mul α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] (a : α) {b : α} {c : α} : a * b < a * c ↔ b < c

ink

@[simp]

theorem add_lt_add_iff_right {α : Type u_1} [inst : Add α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b : α} {c : α} : b + a < c + a ↔ b < c

ink

@[simp]

theorem mul_lt_mul_iff_right {α : Type u_1} [inst : Mul α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] (a : α) {b : α} {c : α} : b * a < c * a ↔ b < c

ink

theorem add_lt_add_left {α : Type u_1} [inst : Add α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {b : α} {c : α} (bc : b < c) (a : α) : a + b < a + c

ink

theorem mul_lt_mul_left' {α : Type u_1} [inst : Mul α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {b : α} {c : α} (bc : b < c) (a : α) : a * b < a * c

ink

theorem lt_of_add_lt_add_left {α : Type u_1} [inst : Add α] [inst : LT α] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} (bc : a + b < a + c) : b < c

ink

theorem lt_of_mul_lt_mul_left' {α : Type u_1} [inst : Mul α] [inst : LT α] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} (bc : a * b < a * c) : b < c

ink

theorem add_lt_add_right {α : Type u_1} [inst : Add α] [inst : LT α] [i : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {b : α} {c : α} (bc : b < c) (a : α) : b + a < c + a

ink

theorem mul_lt_mul_right' {α : Type u_1} [inst : Mul α] [inst : LT α] [i : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {b : α} {c : α} (bc : b < c) (a : α) : b * a < c * a

ink

theorem lt_of_add_lt_add_right {α : Type u_1} [inst : Add α] [inst : LT α] [i : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} (bc : b + a < c + a) : b < c

ink

theorem lt_of_mul_lt_mul_right' {α : Type u_1} [inst : Mul α] [inst : LT α] [i : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} (bc : b * a < c * a) : b < c

ink

theorem add_lt_add_of_lt_of_lt {α : Type u_1} [inst : Add α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} {d : α} (h₁ : a < b) (h₂ : c < d) : a + c < b + d

ink

theorem mul_lt_mul_of_lt_of_lt {α : Type u_1} [inst : Mul α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} {d : α} (h₁ : a < b) (h₂ : c < d) : a * c < b * d

ink

theorem add_lt_add {α : Type u_1} [inst : Add α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} {d : α} (h₁ : a < b) (h₂ : c < d) : a + c < b + d

Alias of add_lt_add_of_lt_of_lt.

ink

theorem add_lt_add_of_le_of_lt {α : Type u_1} [inst : Add α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (h₁ : a ≤ b) (h₂ : c < d) : a + c < b + d

ink

theorem mul_lt_mul_of_le_of_lt {α : Type u_1} [inst : Mul α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (h₁ : a ≤ b) (h₂ : c < d) : a * c < b * d

ink

theorem add_lt_add_of_lt_of_le {α : Type u_1} [inst : Add α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} {d : α} (h₁ : a < b) (h₂ : c ≤ d) : a + c < b + d

ink

theorem mul_lt_mul_of_lt_of_le {α : Type u_1} [inst : Mul α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} {d : α} (h₁ : a < b) (h₂ : c ≤ d) : a * c < b * d

ink

theorem Left.add_lt_add {α : Type u_1} [inst : Add α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (h₁ : a < b) (h₂ : c < d) : a + c < b + d

Only assumes left strict covariance

ink

theorem Left.mul_lt_mul {α : Type u_1} [inst : Mul α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (h₁ : a < b) (h₂ : c < d) : a * c < b * d

Only assumes left strict covariance.

ink

theorem Right.add_lt_add {α : Type u_1} [inst : Add α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} {d : α} (h₁ : a < b) (h₂ : c < d) : a + c < b + d

Only assumes right strict covariance

ink

theorem Right.mul_lt_mul {α : Type u_1} [inst : Mul α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} {d : α} (h₁ : a < b) (h₂ : c < d) : a * c < b * d

Only assumes right strict covariance.

ink

theorem add_le_add {α : Type u_1} [inst : Add α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d

ink

theorem mul_le_mul' {α : Type u_1} [inst : Mul α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) : a * c ≤ b * d

ink

theorem add_le_add_three {α : Type u_1} [inst : Add α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} {e : α} {f : α} (h₁ : a ≤ d) (h₂ : b ≤ e) (h₃ : c ≤ f) : a + b + c ≤ d + e + f

ink

theorem mul_le_mul_three {α : Type u_1} [inst : Mul α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} {e : α} {f : α} (h₁ : a ≤ d) (h₂ : b ≤ e) (h₃ : c ≤ f) : a * b * c ≤ d * e * f

ink

theorem add_lt_of_add_lt_left {α : Type u_1} [inst : Add α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (h : a + b < c) (hle : d ≤ b) : a + d < c

ink

theorem mul_lt_of_mul_lt_left {α : Type u_1} [inst : Mul α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (h : a * b < c) (hle : d ≤ b) : a * d < c

ink

theorem add_le_of_add_le_left {α : Type u_1} [inst : Add α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (h : a + b ≤ c) (hle : d ≤ b) : a + d ≤ c

ink

theorem mul_le_of_mul_le_left {α : Type u_1} [inst : Mul α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (h : a * b ≤ c) (hle : d ≤ b) : a * d ≤ c

ink

theorem add_lt_of_add_lt_right {α : Type u_1} [inst : Add α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (h : a + b < c) (hle : d ≤ a) : d + b < c

ink

theorem mul_lt_of_mul_lt_right {α : Type u_1} [inst : Mul α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (h : a * b < c) (hle : d ≤ a) : d * b < c

ink

theorem add_le_of_add_le_right {α : Type u_1} [inst : Add α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (h : a + b ≤ c) (hle : d ≤ a) : d + b ≤ c

ink

theorem mul_le_of_mul_le_right {α : Type u_1} [inst : Mul α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (h : a * b ≤ c) (hle : d ≤ a) : d * b ≤ c

ink

theorem lt_add_of_lt_add_left {α : Type u_1} [inst : Add α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (h : a < b + c) (hle : c ≤ d) : a < b + d

ink

theorem lt_mul_of_lt_mul_left {α : Type u_1} [inst : Mul α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (h : a < b * c) (hle : c ≤ d) : a < b * d

ink

theorem le_add_of_le_add_left {α : Type u_1} [inst : Add α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (h : a ≤ b + c) (hle : c ≤ d) : a ≤ b + d

ink

theorem le_mul_of_le_mul_left {α : Type u_1} [inst : Mul α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (h : a ≤ b * c) (hle : c ≤ d) : a ≤ b * d

ink

theorem lt_add_of_lt_add_right {α : Type u_1} [inst : Add α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (h : a < b + c) (hle : b ≤ d) : a < d + c

ink

theorem lt_mul_of_lt_mul_right {α : Type u_1} [inst : Mul α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (h : a < b * c) (hle : b ≤ d) : a < d * c

ink

theorem le_add_of_le_add_right {α : Type u_1} [inst : Add α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (h : a ≤ b + c) (hle : b ≤ d) : a ≤ d + c

ink

theorem le_mul_of_le_mul_right {α : Type u_1} [inst : Mul α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (h : a ≤ b * c) (hle : b ≤ d) : a ≤ d * c

ink

theorem add_left_cancel'' {α : Type u_1} [inst : Add α] [inst : PartialOrder α] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (h : a + b = a + c) : b = c

ink

theorem mul_left_cancel'' {α : Type u_1} [inst : Mul α] [inst : PartialOrder α] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (h : a * b = a * c) : b = c

ink

theorem add_right_cancel'' {α : Type u_1} [inst : Add α] [inst : PartialOrder α] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (h : a + b = c + b) : a = c

ink

theorem mul_right_cancel'' {α : Type u_1} [inst : Mul α] [inst : PartialOrder α] [inst : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (h : a * b = c * b) : a = c

ink

theorem min_le_max_of_add_le_add {α : Type u_1} [inst : Add α] [inst : LinearOrder α] {a : α} {b : α} {c : α} {d : α} [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (h : a + b ≤ c + d) : min a b ≤ max c d

ink

theorem min_le_max_of_mul_le_mul {α : Type u_1} [inst : Mul α] [inst : LinearOrder α] {a : α} {b : α} {c : α} {d : α} [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] (h : a * b ≤ c * d) : min a b ≤ max c d

ink

theorem le_add_of_nonneg_right {α : Type u_1} [inst : AddZeroClass α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (h : 0 ≤ b) : a ≤ a + b

ink

theorem le_mul_of_one_le_right' {α : Type u_1} [inst : MulOneClass α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (h : 1 ≤ b) : a ≤ a * b

ink

theorem add_le_of_nonpos_right {α : Type u_1} [inst : AddZeroClass α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (h : b ≤ 0) : a + b ≤ a

ink

theorem mul_le_of_le_one_right' {α : Type u_1} [inst : MulOneClass α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (h : b ≤ 1) : a * b ≤ a

ink

theorem le_add_of_nonneg_left {α : Type u_1} [inst : AddZeroClass α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (h : 0 ≤ b) : a ≤ b + a

ink

theorem le_mul_of_one_le_left' {α : Type u_1} [inst : MulOneClass α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (h : 1 ≤ b) : a ≤ b * a

ink

theorem add_le_of_nonpos_left {α : Type u_1} [inst : AddZeroClass α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (h : b ≤ 0) : b + a ≤ a

ink

theorem mul_le_of_le_one_left' {α : Type u_1} [inst : MulOneClass α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (h : b ≤ 1) : b * a ≤ a

ink

theorem nonneg_of_le_add_right {α : Type u_1} [inst : AddZeroClass α] [inst : LE α] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (h : a ≤ a + b) : 0 ≤ b

ink

theorem one_le_of_le_mul_right {α : Type u_1} [inst : MulOneClass α] [inst : LE α] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (h : a ≤ a * b) : 1 ≤ b

ink

theorem nonpos_of_add_le_right {α : Type u_1} [inst : AddZeroClass α] [inst : LE α] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (h : a + b ≤ a) : b ≤ 0

ink

theorem le_one_of_mul_le_right {α : Type u_1} [inst : MulOneClass α] [inst : LE α] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (h : a * b ≤ a) : b ≤ 1

ink

theorem nonneg_of_le_add_left {α : Type u_1} [inst : AddZeroClass α] [inst : LE α] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (h : b ≤ a + b) : 0 ≤ a

ink

theorem one_le_of_le_mul_left {α : Type u_1} [inst : MulOneClass α] [inst : LE α] [inst : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (h : b ≤ a * b) : 1 ≤ a

ink

theorem nonpos_of_add_le_left {α : Type u_1} [inst : AddZeroClass α] [inst : LE α] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (h : a + b ≤ b) : a ≤ 0

ink

theorem le_one_of_mul_le_left {α : Type u_1} [inst : MulOneClass α] [inst : LE α] [inst : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (h : a * b ≤ b) : a ≤ 1

ink

@[simp]

theorem le_add_iff_nonneg_right {α : Type u_1} [inst : AddZeroClass α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) {b : α} : a ≤ a + b ↔ 0 ≤ b

ink

@[simp]

theorem le_mul_iff_one_le_right' {α : Type u_1} [inst : MulOneClass α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (a : α) {b : α} : a ≤ a * b ↔ 1 ≤ b

ink

@[simp]

theorem le_add_iff_nonneg_left {α : Type u_1} [inst : AddZeroClass α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) {b : α} : a ≤ b + a ↔ 0 ≤ b

ink

@[simp]

theorem le_mul_iff_one_le_left' {α : Type u_1} [inst : MulOneClass α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (a : α) {b : α} : a ≤ b * a ↔ 1 ≤ b

ink

@[simp]

theorem add_le_iff_nonpos_right {α : Type u_1} [inst : AddZeroClass α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) {b : α} : a + b ≤ a ↔ b ≤ 0

ink

@[simp]

theorem mul_le_iff_le_one_right' {α : Type u_1} [inst : MulOneClass α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (a : α) {b : α} : a * b ≤ a ↔ b ≤ 1

ink

@[simp]

theorem add_le_iff_nonpos_left {α : Type u_1} [inst : AddZeroClass α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : a + b ≤ b ↔ a ≤ 0

ink

@[simp]

theorem mul_le_iff_le_one_left' {α : Type u_1} [inst : MulOneClass α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} : a * b ≤ b ↔ a ≤ 1

ink

theorem lt_add_of_pos_right {α : Type u_1} [inst : AddZeroClass α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b : α} (h : 0 < b) : a < a + b

ink

theorem lt_mul_of_one_lt_right' {α : Type u_1} [inst : MulOneClass α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] (a : α) {b : α} (h : 1 < b) : a < a * b

ink

theorem add_lt_of_neg_right {α : Type u_1} [inst : AddZeroClass α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b : α} (h : b < 0) : a + b < a

ink

theorem mul_lt_of_lt_one_right' {α : Type u_1} [inst : MulOneClass α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] (a : α) {b : α} (h : b < 1) : a * b < a

ink

theorem lt_add_of_pos_left {α : Type u_1} [inst : AddZeroClass α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b : α} (h : 0 < b) : a < b + a

ink

theorem lt_mul_of_one_lt_left' {α : Type u_1} [inst : MulOneClass α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] (a : α) {b : α} (h : 1 < b) : a < b * a

ink

theorem add_lt_of_neg_left {α : Type u_1} [inst : AddZeroClass α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b : α} (h : b < 0) : b + a < a

ink

theorem mul_lt_of_lt_one_left' {α : Type u_1} [inst : MulOneClass α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] (a : α) {b : α} (h : b < 1) : b * a < a

ink

theorem pos_of_lt_add_right {α : Type u_1} [inst : AddZeroClass α] [inst : LT α] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : a < a + b) : 0 < b

ink

theorem one_lt_of_lt_mul_right {α : Type u_1} [inst : MulOneClass α] [inst : LT α] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : a < a * b) : 1 < b

ink

theorem neg_of_add_lt_right {α : Type u_1} [inst : AddZeroClass α] [inst : LT α] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : a + b < a) : b < 0

ink

theorem lt_one_of_mul_lt_right {α : Type u_1} [inst : MulOneClass α] [inst : LT α] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : a * b < a) : b < 1

ink

theorem pos_of_lt_add_left {α : Type u_1} [inst : AddZeroClass α] [inst : LT α] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : b < a + b) : 0 < a

ink

theorem one_lt_of_lt_mul_left {α : Type u_1} [inst : MulOneClass α] [inst : LT α] [inst : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : b < a * b) : 1 < a

ink

theorem neg_of_add_lt_left {α : Type u_1} [inst : AddZeroClass α] [inst : LT α] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : a + b < b) : a < 0

ink

theorem lt_one_of_mul_lt_left {α : Type u_1} [inst : MulOneClass α] [inst : LT α] [inst : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : a * b < b) : a < 1

ink

@[simp]

theorem lt_add_iff_pos_right {α : Type u_1} [inst : AddZeroClass α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b : α} : a < a + b ↔ 0 < b

ink

@[simp]

theorem lt_mul_iff_one_lt_right' {α : Type u_1} [inst : MulOneClass α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] (a : α) {b : α} : a < a * b ↔ 1 < b

ink

@[simp]

theorem lt_add_iff_pos_left {α : Type u_1} [inst : AddZeroClass α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b : α} : a < b + a ↔ 0 < b

ink

@[simp]

theorem lt_mul_iff_one_lt_left' {α : Type u_1} [inst : MulOneClass α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] (a : α) {b : α} : a < b * a ↔ 1 < b

ink

@[simp]

theorem add_lt_iff_neg_left {α : Type u_1} [inst : AddZeroClass α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} : a + b < a ↔ b < 0

ink

@[simp]

theorem mul_lt_iff_lt_one_left' {α : Type u_1} [inst : MulOneClass α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} : a * b < a ↔ b < 1

ink

@[simp]

theorem add_lt_iff_neg_right {α : Type u_1} [inst : AddZeroClass α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} (b : α) : a + b < b ↔ a < 0

ink

@[simp]

theorem mul_lt_iff_lt_one_right' {α : Type u_1} [inst : MulOneClass α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} (b : α) : a * b < b ↔ a < 1

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

ink

theorem add_le_of_le_of_nonpos {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (hbc : b ≤ c) (ha : a ≤ 0) : b + a ≤ c

ink

theorem mul_le_of_le_of_le_one {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (hbc : b ≤ c) (ha : a ≤ 1) : b * a ≤ c

ink

theorem add_lt_of_le_of_neg {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} (hbc : b ≤ c) (ha : a < 0) : b + a < c

ink

theorem mul_lt_of_le_of_lt_one {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} (hbc : b ≤ c) (ha : a < 1) : b * a < c

ink

theorem add_lt_of_lt_of_nonpos {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (hbc : b < c) (ha : a ≤ 0) : b + a < c

ink

theorem mul_lt_of_lt_of_le_one {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (hbc : b < c) (ha : a ≤ 1) : b * a < c

ink

theorem add_lt_of_lt_of_neg {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} (hbc : b < c) (ha : a < 0) : b + a < c

ink

theorem mul_lt_of_lt_of_lt_one {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} (hbc : b < c) (ha : a < 1) : b * a < c

ink

theorem add_lt_of_lt_of_neg' {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (hbc : b < c) (ha : a < 0) : b + a < c

ink

theorem mul_lt_of_lt_of_lt_one' {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (hbc : b < c) (ha : a < 1) : b * a < c

ink

theorem Left.add_nonpos {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : a ≤ 0) (hb : b ≤ 0) : a + b ≤ 0

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

ink

theorem Left.mul_le_one {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : a ≤ 1) (hb : b ≤ 1) : a * b ≤ 1

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

ink

theorem Left.add_neg_of_nonpos_of_neg {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {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.

ink

theorem Left.mul_lt_one_of_le_of_lt {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {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.

ink

theorem Left.add_neg_of_neg_of_nonpos {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {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.

ink

theorem Left.mul_lt_one_of_lt_of_le {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {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.

ink

theorem Left.add_neg {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} (ha : a < 0) (hb : b < 0) : a + b < 0

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

ink

theorem Left.mul_lt_one {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} (ha : a < 1) (hb : b < 1) : a * b < 1

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

ink

theorem Left.add_neg' {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : a < 0) (hb : b < 0) : a + b < 0

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

ink

theorem Left.mul_lt_one' {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {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≤ c → 1 ≤ a → b ≤ c * a→ 1 ≤ a → b ≤ c * a≤ a → b ≤ c * a→ b ≤ c * a≤ c * a, which assume left covariance.

ink

theorem le_add_of_le_of_nonneg {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (hbc : b ≤ c) (ha : 0 ≤ a) : b ≤ c + a

ink

theorem le_mul_of_le_of_one_le {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (hbc : b ≤ c) (ha : 1 ≤ a) : b ≤ c * a

ink

theorem lt_add_of_le_of_pos {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} (hbc : b ≤ c) (ha : 0 < a) : b < c + a

ink

theorem lt_mul_of_le_of_one_lt {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} (hbc : b ≤ c) (ha : 1 < a) : b < c * a

ink

theorem lt_add_of_lt_of_nonneg {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (hbc : b < c) (ha : 0 ≤ a) : b < c + a

ink

theorem lt_mul_of_lt_of_one_le {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (hbc : b < c) (ha : 1 ≤ a) : b < c * a

ink

theorem lt_add_of_lt_of_pos {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} (hbc : b < c) (ha : 0 < a) : b < c + a

ink

theorem lt_mul_of_lt_of_one_lt {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} (hbc : b < c) (ha : 1 < a) : b < c * a

ink

theorem lt_add_of_lt_of_pos' {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (hbc : b < c) (ha : 0 < a) : b < c + a

ink

theorem lt_mul_of_lt_of_one_lt' {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (hbc : b < c) (ha : 1 < a) : b < c * a

ink

theorem Left.add_nonneg {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a + b

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

ink

theorem Left.one_le_mul {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ a * b

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

ink

theorem Left.add_pos_of_nonneg_of_pos {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {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.

ink

theorem Left.one_lt_mul_of_le_of_lt {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {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.

ink

theorem Left.add_pos_of_pos_of_nonneg {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {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.

ink

theorem Left.one_lt_mul_of_lt_of_le {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {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.

ink

theorem Left.add_pos {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} (ha : 0 < a) (hb : 0 < b) : 0 < a + b

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

ink

theorem Left.one_lt_mul {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} (ha : 1 < a) (hb : 1 < b) : 1 < a * b

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

ink

theorem Left.add_pos' {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 0 < a) (hb : 0 < b) : 0 < a + b

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

ink

theorem Left.one_lt_mul' {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {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≤ 1 → b ≤ c → a * b ≤ c→ b ≤ c → a * b ≤ c≤ c → a * b ≤ c→ a * b ≤ c≤ c, which assume right covariance.

ink

theorem add_le_of_nonpos_of_le {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (ha : a ≤ 0) (hbc : b ≤ c) : a + b ≤ c

ink

theorem mul_le_of_le_one_of_le {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (ha : a ≤ 1) (hbc : b ≤ c) : a * b ≤ c

ink

theorem add_lt_of_neg_of_le {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} (ha : a < 0) (hbc : b ≤ c) : a + b < c

ink

theorem mul_lt_of_lt_one_of_le {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} (ha : a < 1) (hbc : b ≤ c) : a * b < c

ink

theorem add_lt_of_nonpos_of_lt {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (ha : a ≤ 0) (hb : b < c) : a + b < c

ink

theorem mul_lt_of_le_one_of_lt {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (ha : a ≤ 1) (hb : b < c) : a * b < c

ink

theorem add_lt_of_neg_of_lt {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} (ha : a < 0) (hb : b < c) : a + b < c

ink

theorem mul_lt_of_lt_one_of_lt {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} (ha : a < 1) (hb : b < c) : a * b < c

ink

theorem add_lt_of_neg_of_lt' {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (ha : a < 0) (hbc : b < c) : a + b < c

ink

theorem mul_lt_of_lt_one_of_lt' {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (ha : a < 1) (hbc : b < c) : a * b < c

ink

theorem Right.add_nonpos {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : a ≤ 0) (hb : b ≤ 0) : a + b ≤ 0

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

ink

theorem Right.mul_le_one {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : a ≤ 1) (hb : b ≤ 1) : a * b ≤ 1

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

ink

theorem Right.add_neg_of_neg_of_nonpos {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {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.

ink

theorem Right.mul_lt_one_of_lt_of_le {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {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.

ink

theorem Right.add_neg_of_nonpos_of_neg {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {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.

ink

theorem Right.mul_lt_one_of_le_of_lt {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {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.

ink

theorem Right.add_neg {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} (ha : a < 0) (hb : b < 0) : a + b < 0

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

ink

theorem Right.mul_lt_one {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} (ha : a < 1) (hb : b < 1) : a * b < 1

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

ink

theorem Right.add_neg' {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : a < 0) (hb : b < 0) : a + b < 0

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

ink

theorem Right.mul_lt_one' {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {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≤ a → b ≤ c → b ≤ a * c→ b ≤ c → b ≤ a * c≤ c → b ≤ a * c→ b ≤ a * c≤ a * c, which assume right covariance.

ink

theorem le_add_of_nonneg_of_le {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (ha : 0 ≤ a) (hbc : b ≤ c) : b ≤ a + c

ink

theorem le_mul_of_one_le_of_le {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (ha : 1 ≤ a) (hbc : b ≤ c) : b ≤ a * c

ink

theorem lt_add_of_pos_of_le {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} (ha : 0 < a) (hbc : b ≤ c) : b < a + c

ink

theorem lt_mul_of_one_lt_of_le {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} (ha : 1 < a) (hbc : b ≤ c) : b < a * c

ink

theorem lt_add_of_nonneg_of_lt {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (ha : 0 ≤ a) (hbc : b < c) : b < a + c

ink

theorem lt_mul_of_one_le_of_lt {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (ha : 1 ≤ a) (hbc : b < c) : b < a * c

ink

theorem lt_add_of_pos_of_lt {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} (ha : 0 < a) (hbc : b < c) : b < a + c

ink

theorem lt_mul_of_one_lt_of_lt {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} (ha : 1 < a) (hbc : b < c) : b < a * c

ink

theorem lt_add_of_pos_of_lt' {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (ha : 0 < a) (hbc : b < c) : b < a + c

ink

theorem lt_mul_of_one_lt_of_lt' {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (ha : 1 < a) (hbc : b < c) : b < a * c

ink

theorem Right.add_nonneg {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a + b

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

ink

theorem Right.one_le_mul {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ a * b

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

ink

theorem Right.add_pos_of_pos_of_nonneg {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {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.

ink

theorem Right.one_lt_mul_of_lt_of_le {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {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.

ink

theorem Right.add_pos_of_nonneg_of_pos {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {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.

ink

theorem Right.one_lt_mul_of_le_of_lt {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {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.

ink

theorem Right.add_pos {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} (ha : 0 < a) (hb : 0 < b) : 0 < a + b

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

ink

theorem Right.one_lt_mul {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} (ha : 1 < a) (hb : 1 < b) : 1 < a * b

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

ink

theorem Right.add_pos' {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 0 < a) (hb : 0 < b) : 0 < a + b

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

ink

theorem Right.one_lt_mul' {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 1 < a) (hb : 1 < b) : 1 < a * b

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

ink

theorem mul_le_one' {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : a ≤ 1) (hb : b ≤ 1) : a * b ≤ 1

Alias of Left.mul_le_one.

ink

theorem mul_lt_one_of_le_of_lt {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} (ha : a ≤ 1) (hb : b < 1) : a * b < 1

Alias of Left.mul_lt_one_of_le_of_lt.

ink

theorem mul_lt_one_of_lt_of_le {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : a < 1) (hb : b ≤ 1) : a * b < 1

Alias of Left.mul_lt_one_of_lt_of_le.

ink

theorem mul_lt_one {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} (ha : a < 1) (hb : b < 1) : a * b < 1

Alias of Left.mul_lt_one.

ink

theorem mul_lt_one' {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : a < 1) (hb : b < 1) : a * b < 1

Alias of Left.mul_lt_one'.

ink

theorem add_nonpos {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : a ≤ 0) (hb : b ≤ 0) : a + b ≤ 0

Alias of Left.add_nonpos.

ink

theorem add_neg_of_nonpos_of_neg {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} (ha : a ≤ 0) (hb : b < 0) : a + b < 0

Alias of Left.add_neg_of_nonpos_of_neg.

ink

theorem add_neg_of_neg_of_nonpos {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : a < 0) (hb : b ≤ 0) : a + b < 0

Alias of Left.add_neg_of_neg_of_nonpos.

ink

theorem add_neg {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} (ha : a < 0) (hb : b < 0) : a + b < 0

Alias of Left.add_neg.

ink

theorem add_neg' {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : a < 0) (hb : b < 0) : a + b < 0

Alias of Left.add_neg'.

ink

theorem one_le_mul {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ a * b

Alias of Left.one_le_mul.

ink

theorem one_lt_mul_of_le_of_lt' {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} (ha : 1 ≤ a) (hb : 1 < b) : 1 < a * b

Alias of Left.one_lt_mul_of_le_of_lt.

ink

theorem one_lt_mul_of_lt_of_le' {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 1 < a) (hb : 1 ≤ b) : 1 < a * b

Alias of Left.one_lt_mul_of_lt_of_le.

ink

theorem one_lt_mul' {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} (ha : 1 < a) (hb : 1 < b) : 1 < a * b

Alias of Left.one_lt_mul.

ink

theorem one_lt_mul'' {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 1 < a) (hb : 1 < b) : 1 < a * b

Alias of Left.one_lt_mul'.

ink

theorem add_nonneg {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a + b

Alias of Left.add_nonneg.

ink

theorem add_pos_of_nonneg_of_pos {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} (ha : 0 ≤ a) (hb : 0 < b) : 0 < a + b

Alias of Left.add_pos_of_nonneg_of_pos.

ink

theorem add_pos_of_pos_of_nonneg {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 0 < a) (hb : 0 ≤ b) : 0 < a + b

Alias of Left.add_pos_of_pos_of_nonneg.

ink

theorem add_pos {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} (ha : 0 < a) (hb : 0 < b) : 0 < a + b

Alias of Left.add_pos.

ink

theorem add_pos' {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 0 < a) (hb : 0 < b) : 0 < a + b

Alias of Left.add_pos'.

ink

theorem lt_of_add_lt_of_nonneg_left {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (h : a + b < c) (hle : 0 ≤ b) : a < c

ink

theorem lt_of_mul_lt_of_one_le_left {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (h : a * b < c) (hle : 1 ≤ b) : a < c

ink

theorem le_of_add_le_of_nonneg_left {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (h : a + b ≤ c) (hle : 0 ≤ b) : a ≤ c

ink

theorem le_of_mul_le_of_one_le_left {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (h : a * b ≤ c) (hle : 1 ≤ b) : a ≤ c

ink

theorem lt_of_lt_add_of_nonpos_left {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (h : a < b + c) (hle : c ≤ 0) : a < b

ink

theorem lt_of_lt_mul_of_le_one_left {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (h : a < b * c) (hle : c ≤ 1) : a < b

ink

theorem le_of_le_add_of_nonpos_left {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (h : a ≤ b + c) (hle : c ≤ 0) : a ≤ b

ink

theorem le_of_le_mul_of_le_one_left {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (h : a ≤ b * c) (hle : c ≤ 1) : a ≤ b

ink

theorem lt_of_add_lt_of_nonneg_right {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (h : a + b < c) (hle : 0 ≤ a) : b < c

ink

theorem lt_of_mul_lt_of_one_le_right {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (h : a * b < c) (hle : 1 ≤ a) : b < c

ink

theorem le_of_add_le_of_nonneg_right {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (h : a + b ≤ c) (hle : 0 ≤ a) : b ≤ c

ink

theorem le_of_mul_le_of_one_le_right {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (h : a * b ≤ c) (hle : 1 ≤ a) : b ≤ c

ink

theorem lt_of_lt_add_of_nonpos_right {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (h : a < b + c) (hle : b ≤ 0) : a < c

ink

theorem lt_of_lt_mul_of_le_one_right {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (h : a < b * c) (hle : b ≤ 1) : a < c

ink

theorem le_of_le_add_of_nonpos_right {α : Type u_1} [inst : AddZeroClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (h : a ≤ b + c) (hle : b ≤ 0) : a ≤ c

ink

theorem le_of_le_mul_of_le_one_right {α : Type u_1} [inst : MulOneClass α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} (h : a ≤ b * c) (hle : b ≤ 1) : a ≤ c

ink

theorem add_eq_zero_iff' {α : Type u_1} [inst : AddZeroClass α] [inst : PartialOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) : a + b = 0 ↔ a = 0 ∧ b = 0

ink

theorem mul_eq_one_iff' {α : Type u_1} [inst : MulOneClass α] [inst : PartialOrder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) : a * b = 1 ↔ a = 1 ∧ b = 1

ink

theorem add_le_add_iff_of_ge {α : Type u_1} [inst : AddZeroClass α] [inst : PartialOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) : a₂ + b₂ ≤ a₁ + b₁ ↔ a₁ = a₂ ∧ b₁ = b₂

ink

theorem mul_le_mul_iff_of_ge {α : Type u_1} [inst : MulOneClass α] [inst : PartialOrder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) : a₂ * b₂ ≤ a₁ * b₁ ↔ a₁ = a₂ ∧ b₁ = b₂

ink

theorem eq_zero_of_add_nonneg_left {α : Type u_1} [inst : AddZeroClass α] [inst : PartialOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : a ≤ 0) (hb : b ≤ 0) (hab : 0 ≤ a + b) : a = 0

ink

theorem eq_one_of_one_le_mul_left {α : Type u_1} [inst : MulOneClass α] [inst : PartialOrder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : a ≤ 1) (hb : b ≤ 1) (hab : 1 ≤ a * b) : a = 1

ink

theorem eq_zero_of_add_nonpos_left {α : Type u_1} [inst : AddZeroClass α] [inst : PartialOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 0) : a = 0

ink

theorem eq_one_of_mul_le_one_left {α : Type u_1} [inst : MulOneClass α] [inst : PartialOrder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) (hab : a * b ≤ 1) : a = 1

ink

theorem eq_zero_of_add_nonneg_right {α : Type u_1} [inst : AddZeroClass α] [inst : PartialOrder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : a ≤ 0) (hb : b ≤ 0) (hab : 0 ≤ a + b) : b = 0

ink

theorem eq_one_of_one_le_mul_right {α : Type u_1} [inst : MulOneClass α] [inst : PartialOrder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : a ≤ 1) (hb : b ≤ 1) (hab : 1 ≤ a * b) : b = 1

ink

theorem eq_zero_of_add_nonpos_right {α : Type u_1} [inst : AddZeroClass α] [inst : PartialOrder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 0) : b = 0

ink

theorem eq_one_of_mul_le_one_right {α : Type u_1} [inst : MulOneClass α] [inst : PartialOrder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) (hab : a * b ≤ 1) : b = 1

ink

theorem exists_square_le {α : Type u_1} [inst : MulOneClass α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] (a : α) : ∃ b, b * b ≤ a

ink

def Contravariant.toAddLeftCancelSemigroup {α : Type u_1} [inst : AddSemigroup α] [inst : PartialOrder α] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] : AddLeftCancelSemigroup α

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

Equations

• Contravariant.toAddLeftCancelSemigroup = let src := inst; AddLeftCancelSemigroup.mk (_ : ∀ (a b c : α), a + b = a + c → b = c)

ink

def Contravariant.toAddLeftCancelSemigroup.proof_1 {α : Type u_1} [inst : AddSemigroup α] [inst : PartialOrder α] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) (b : α) (c : α) (h : a + b = a + c) : b = c

Equations

• (_ : a + b = a + c → b = c) = (_ : a + b = a + c → b = c)

ink

def Contravariant.toLeftCancelSemigroup {α : Type u_1} [inst : Semigroup α] [inst : PartialOrder α] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] : LeftCancelSemigroup α

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

Equations

• Contravariant.toLeftCancelSemigroup = let src := inst; LeftCancelSemigroup.mk (_ : ∀ (a b c : α), a * b = a * c → b = c)

ink

def Contravariant.toAddRightCancelSemigroup.proof_1 {α : Type u_1} [inst : AddSemigroup α] [inst : PartialOrder α] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) (b : α) (c : α) (h : a + b = c + b) : a = c

Equations

• (_ : a + b = c + b → a = c) = (_ : a + b = c + b → a = c)

ink

def Contravariant.toAddRightCancelSemigroup {α : Type u_1} [inst : AddSemigroup α] [inst : PartialOrder α] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] : AddRightCancelSemigroup α

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

Equations

• Contravariant.toAddRightCancelSemigroup = let src := inst; AddRightCancelSemigroup.mk (_ : ∀ (a b c : α), a + b = c + b → a = c)

ink

def Contravariant.toRightCancelSemigroup {α : Type u_1} [inst : Semigroup α] [inst : PartialOrder α] [inst : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] : RightCancelSemigroup α

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

Equations

• Contravariant.toRightCancelSemigroup = let src := inst; RightCancelSemigroup.mk (_ : ∀ (a b c : α), a * b = c * b → a = c)

ink

theorem Left.add_eq_add_iff_eq_and_eq {α : Type u_1} [inst : AddSemigroup α] [inst : PartialOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (hac : a ≤ c) (hbd : b ≤ d) : a + b = c + d ↔ a = c ∧ b = d

ink

theorem Left.mul_eq_mul_iff_eq_and_eq {α : Type u_1} [inst : Semigroup α] [inst : PartialOrder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (hac : a ≤ c) (hbd : b ≤ d) : a * b = c * d ↔ a = c ∧ b = d

ink

theorem Right.add_eq_add_iff_eq_and_eq {α : Type u_1} [inst : AddSemigroup α] [inst : PartialOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (hac : a ≤ c) (hbd : b ≤ d) : a + b = c + d ↔ a = c ∧ b = d

ink

theorem Right.mul_eq_mul_iff_eq_and_eq {α : Type u_1} [inst : Semigroup α] [inst : PartialOrder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (hac : a ≤ c) (hbd : b ≤ d) : a * b = c * d ↔ a = c ∧ b = d

ink

theorem mul_eq_mul_iff_eq_and_eq {α : Type u_1} [inst : Semigroup α] [inst : PartialOrder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (hac : a ≤ c) (hbd : b ≤ d) : a * b = c * d ↔ a = c ∧ b = d

Alias of Left.mul_eq_mul_iff_eq_and_eq.

ink

theorem add_eq_add_iff_eq_and_eq {α : Type u_1} [inst : AddSemigroup α] [inst : PartialOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (hac : a ≤ c) (hbd : b ≤ d) : a + b = c + d ↔ a = c ∧ b = d

ink

theorem Monotone.const_add {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Preorder α] [inst : Preorder β] {f : β → α} [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (hf : Monotone f) (a : α) : Monotone fun x => a + f x

ink

theorem Monotone.const_mul' {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst : Preorder α] [inst : Preorder β] {f : β → α} [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (hf : Monotone f) (a : α) : Monotone fun x => a * f x

ink

theorem MonotoneOn.const_add {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {s : Set β} [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (hf : MonotoneOn f s) (a : α) : MonotoneOn (fun x => a + f x) s

ink

theorem MonotoneOn.const_mul' {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {s : Set β} [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (hf : MonotoneOn f s) (a : α) : MonotoneOn (fun x => a * f x) s

ink

theorem Antitone.const_add {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Preorder α] [inst : Preorder β] {f : β → α} [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (hf : Antitone f) (a : α) : Antitone fun x => a + f x

ink

theorem Antitone.const_mul' {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst : Preorder α] [inst : Preorder β] {f : β → α} [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (hf : Antitone f) (a : α) : Antitone fun x => a * f x

ink

theorem AntitoneOn.const_add {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {s : Set β} [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (hf : AntitoneOn f s) (a : α) : AntitoneOn (fun x => a + f x) s

ink

theorem AntitoneOn.const_mul' {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {s : Set β} [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (hf : AntitoneOn f s) (a : α) : AntitoneOn (fun x => a * f x) s

ink

theorem Monotone.add_const {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Preorder α] [inst : Preorder β] {f : β → α} [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (hf : Monotone f) (a : α) : Monotone fun x => f x + a

ink

theorem Monotone.mul_const' {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst : Preorder α] [inst : Preorder β] {f : β → α} [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (hf : Monotone f) (a : α) : Monotone fun x => f x * a

ink

theorem MonotoneOn.add_const {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {s : Set β} [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (hf : MonotoneOn f s) (a : α) : MonotoneOn (fun x => f x + a) s

ink

theorem MonotoneOn.mul_const' {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {s : Set β} [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (hf : MonotoneOn f s) (a : α) : MonotoneOn (fun x => f x * a) s

ink

theorem Antitone.add_const {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Preorder α] [inst : Preorder β] {f : β → α} [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (hf : Antitone f) (a : α) : Antitone fun x => f x + a

ink

theorem Antitone.mul_const' {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst : Preorder α] [inst : Preorder β] {f : β → α} [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (hf : Antitone f) (a : α) : Antitone fun x => f x * a

ink

theorem AntitoneOn.add_const {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {s : Set β} [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (hf : AntitoneOn f s) (a : α) : AntitoneOn (fun x => f x + a) s

ink

theorem AntitoneOn.mul_const' {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {s : Set β} [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (hf : AntitoneOn f s) (a : α) : AntitoneOn (fun x => f x * a) s

ink

theorem Monotone.add {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {g : β → α} [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (hf : Monotone f) (hg : Monotone g) : Monotone fun x => f x + g x

The sum of two monotone functions is monotone.

ink

theorem Monotone.mul' {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {g : β → α} [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (hf : Monotone f) (hg : Monotone g) : Monotone fun x => f x * g x

The product of two monotone functions is monotone.

ink

theorem MonotoneOn.add {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {g : β → α} {s : Set β} [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (hf : MonotoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => f x + g x) s

The sum of two monotone functions is monotone.

ink

theorem MonotoneOn.mul' {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {g : β → α} {s : Set β} [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (hf : MonotoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => f x * g x) s

The product of two monotone functions is monotone.

ink

theorem Antitone.add {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {g : β → α} [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (hf : Antitone f) (hg : Antitone g) : Antitone fun x => f x + g x

The sum of two antitone functions is antitone.

ink

theorem Antitone.mul' {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {g : β → α} [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (hf : Antitone f) (hg : Antitone g) : Antitone fun x => f x * g x

The product of two antitone functions is antitone.

ink

theorem AntitoneOn.add {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {g : β → α} {s : Set β} [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (hf : AntitoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun x => f x + g x) s

The sum of two antitone functions is antitone.

ink

theorem AntitoneOn.mul' {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {g : β → α} {s : Set β} [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (hf : AntitoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun x => f x * g x) s

The product of two antitone functions is antitone.

ink

theorem StrictMono.const_add {α : Type u_2} {β : Type u_1} [inst : Add α] [inst : Preorder α] [inst : Preorder β] {f : β → α} [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (hf : StrictMono f) (c : α) : StrictMono fun x => c + f x

ink

theorem StrictMono.const_mul' {α : Type u_2} {β : Type u_1} [inst : Mul α] [inst : Preorder α] [inst : Preorder β] {f : β → α} [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] (hf : StrictMono f) (c : α) : StrictMono fun x => c * f x

ink

theorem StrictMonoOn.const_add {α : Type u_2} {β : Type u_1} [inst : Add α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {s : Set β} [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (hf : StrictMonoOn f s) (c : α) : StrictMonoOn (fun x => c + f x) s

ink

theorem StrictMonoOn.const_mul' {α : Type u_2} {β : Type u_1} [inst : Mul α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {s : Set β} [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] (hf : StrictMonoOn f s) (c : α) : StrictMonoOn (fun x => c * f x) s

ink

theorem StrictAnti.const_add {α : Type u_2} {β : Type u_1} [inst : Add α] [inst : Preorder α] [inst : Preorder β] {f : β → α} [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (hf : StrictAnti f) (c : α) : StrictAnti fun x => c + f x

ink

theorem StrictAnti.const_mul' {α : Type u_2} {β : Type u_1} [inst : Mul α] [inst : Preorder α] [inst : Preorder β] {f : β → α} [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] (hf : StrictAnti f) (c : α) : StrictAnti fun x => c * f x

ink

theorem StrictAntiOn.const_add {α : Type u_2} {β : Type u_1} [inst : Add α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {s : Set β} [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (hf : StrictAntiOn f s) (c : α) : StrictAntiOn (fun x => c + f x) s

ink

theorem StrictAntiOn.const_mul' {α : Type u_2} {β : Type u_1} [inst : Mul α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {s : Set β} [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] (hf : StrictAntiOn f s) (c : α) : StrictAntiOn (fun x => c * f x) s

ink

theorem StrictMono.add_const {α : Type u_2} {β : Type u_1} [inst : Add α] [inst : Preorder α] [inst : Preorder β] {f : β → α} [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (hf : StrictMono f) (c : α) : StrictMono fun x => f x + c

ink

theorem StrictMono.mul_const' {α : Type u_2} {β : Type u_1} [inst : Mul α] [inst : Preorder α] [inst : Preorder β] {f : β → α} [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] (hf : StrictMono f) (c : α) : StrictMono fun x => f x * c

ink

theorem StrictMonoOn.add_const {α : Type u_2} {β : Type u_1} [inst : Add α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {s : Set β} [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (hf : StrictMonoOn f s) (c : α) : StrictMonoOn (fun x => f x + c) s

ink

theorem StrictMonoOn.mul_const' {α : Type u_2} {β : Type u_1} [inst : Mul α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {s : Set β} [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] (hf : StrictMonoOn f s) (c : α) : StrictMonoOn (fun x => f x * c) s

ink

theorem StrictAnti.add_const {α : Type u_2} {β : Type u_1} [inst : Add α] [inst : Preorder α] [inst : Preorder β] {f : β → α} [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (hf : StrictAnti f) (c : α) : StrictAnti fun x => f x + c

ink

theorem StrictAnti.mul_const' {α : Type u_2} {β : Type u_1} [inst : Mul α] [inst : Preorder α] [inst : Preorder β] {f : β → α} [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] (hf : StrictAnti f) (c : α) : StrictAnti fun x => f x * c

ink

theorem StrictAntiOn.add_const {α : Type u_2} {β : Type u_1} [inst : Add α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {s : Set β} [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (hf : StrictAntiOn f s) (c : α) : StrictAntiOn (fun x => f x + c) s

ink

theorem StrictAntiOn.mul_const' {α : Type u_2} {β : Type u_1} [inst : Mul α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {s : Set β} [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] (hf : StrictAntiOn f s) (c : α) : StrictAntiOn (fun x => f x * c) s

ink

theorem StrictMono.add {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {g : β → α} [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (hf : StrictMono f) (hg : StrictMono g) : StrictMono fun x => f x + g x

The sum of two strictly monotone functions is strictly monotone.

ink

theorem StrictMono.mul' {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {g : β → α} [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] (hf : StrictMono f) (hg : StrictMono g) : StrictMono fun x => f x * g x

The product of two strictly monotone functions is strictly monotone.

ink

theorem StrictMonoOn.add {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {g : β → α} {s : Set β} [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (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.

ink

theorem StrictMonoOn.mul' {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst : Preorder α] [inst : Preorder β] {f : β → α} {g : β → α} {s : Set β} [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] (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.

ink

theorem StrictAnti.add {α : Type u_1} {β : Type u_2} [inst : Add α]