mathlib documentation

algebra.order.monoid_lemmas

Ordered monoids #

This file develops the basics of ordered monoids.

Implementation details #

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

Remark #

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

theorem mul_le_mul_left' {α : Type u_1} [has_mul α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {b c : α} (bc : b c) (a : α) :
a * b a * c
theorem add_le_add_left {α : Type u_1} [has_add α] [has_le α] [covariant_class α α has_add.add has_le.le] {b c : α} (bc : b c) (a : α) :
a + b a + c
theorem le_of_mul_le_mul_left' {α : Type u_1} [has_mul α] [has_le α] [contravariant_class α α has_mul.mul has_le.le] {a b c : α} (bc : a * b a * c) :
b c
theorem le_of_add_le_add_left {α : Type u_1} [has_add α] [has_le α] [contravariant_class α α has_add.add has_le.le] {a b c : α} (bc : a + b a + c) :
b c
theorem add_le_add_right {α : Type u_1} [has_add α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {b c : α} (bc : b c) (a : α) :
b + a c + a
theorem mul_le_mul_right' {α : Type u_1} [has_mul α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {b c : α} (bc : b c) (a : α) :
b * a c * a
theorem le_of_mul_le_mul_right' {α : Type u_1} [has_mul α] [has_le α] [contravariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} (bc : b * a c * a) :
b c
theorem le_of_add_le_add_right {α : Type u_1} [has_add α] [has_le α] [contravariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} (bc : b + a c + a) :
b c
@[simp]
theorem mul_le_mul_iff_left {α : Type u_1} [has_mul α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [contravariant_class α α has_mul.mul has_le.le] (a : α) {b c : α} :
a * b a * c b c
@[simp]
theorem add_le_add_iff_left {α : Type u_1} [has_add α] [has_le α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_le.le] (a : α) {b c : α} :
a + b a + c b c
@[simp]
theorem mul_le_mul_iff_right {α : Type u_1} [has_mul α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] [contravariant_class α α (function.swap has_mul.mul) has_le.le] (a : α) {b c : α} :
b * a c * a b c
@[simp]
theorem add_le_add_iff_right {α : Type u_1} [has_add α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] [contravariant_class α α (function.swap has_add.add) has_le.le] (a : α) {b c : α} :
b + a c + a b c
@[simp]
theorem mul_lt_mul_iff_left {α : Type u_1} [has_mul α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [contravariant_class α α has_mul.mul has_lt.lt] (a : α) {b c : α} :
a * b < a * c b < c
@[simp]
theorem add_lt_add_iff_left {α : Type u_1} [has_add α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [contravariant_class α α has_add.add has_lt.lt] (a : α) {b c : α} :
a + b < a + c b < c
@[simp]
theorem mul_lt_mul_iff_right {α : Type u_1} [has_mul α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] [contravariant_class α α (function.swap has_mul.mul) has_lt.lt] (a : α) {b c : α} :
b * a < c * a b < c
@[simp]
theorem add_lt_add_iff_right {α : Type u_1} [has_add α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] [contravariant_class α α (function.swap has_add.add) has_lt.lt] (a : α) {b c : α} :
b + a < c + a b < c
theorem add_lt_add_left {α : Type u_1} [has_add α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {b c : α} (bc : b < c) (a : α) :
a + b < a + c
theorem mul_lt_mul_left' {α : Type u_1} [has_mul α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {b c : α} (bc : b < c) (a : α) :
a * b < a * c
theorem lt_of_add_lt_add_left {α : Type u_1} [has_add α] [has_lt α] [contravariant_class α α has_add.add has_lt.lt] {a b c : α} (bc : a + b < a + c) :
b < c
theorem lt_of_mul_lt_mul_left' {α : Type u_1} [has_mul α] [has_lt α] [contravariant_class α α has_mul.mul has_lt.lt] {a b c : α} (bc : a * b < a * c) :
b < c
theorem mul_lt_mul_right' {α : Type u_1} [has_mul α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {b c : α} (bc : b < c) (a : α) :
b * a < c * a
theorem add_lt_add_right {α : Type u_1} [has_add α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {b c : α} (bc : b < c) (a : α) :
b + a < c + a
theorem lt_of_add_lt_add_right {α : Type u_1} [has_add α] [has_lt α] [contravariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} (bc : b + a < c + a) :
b < c
theorem lt_of_mul_lt_mul_right' {α : Type u_1} [has_mul α] [has_lt α] [contravariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c : α} (bc : b * a < c * a) :
b < c
theorem mul_lt_mul_of_lt_of_lt {α : Type u_1} [has_mul α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c d : α} (h₁ : a < b) (h₂ : c < d) :
a * c < b * d
theorem add_lt_add_of_lt_of_lt {α : Type u_1} [has_add α] [preorder α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c d : α} (h₁ : a < b) (h₂ : c < d) :
a + c < b + d
theorem add_lt_add {α : Type u_1} [has_add α] [preorder α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c d : α} (h₁ : a < b) (h₂ : c < d) :
a + c < b + d

Alias of add_lt_add_of_lt_of_lt.

theorem mul_lt_mul_of_le_of_lt {α : Type u_1} [has_mul α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c d : α} (h₁ : a b) (h₂ : c < d) :
a * c < b * d
theorem add_lt_add_of_le_of_lt {α : Type u_1} [has_add α] [preorder α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c d : α} (h₁ : a b) (h₂ : c < d) :
a + c < b + d
theorem add_lt_add_of_lt_of_le {α : Type u_1} [has_add α] [preorder α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c d : α} (h₁ : a < b) (h₂ : c d) :
a + c < b + d
theorem mul_lt_mul_of_lt_of_le {α : Type u_1} [has_mul α] [preorder α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c d : α} (h₁ : a < b) (h₂ : c d) :
a * c < b * d
theorem left.mul_lt_mul {α : Type u_1} [has_mul α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c d : α} (h₁ : a < b) (h₂ : c < d) :
a * c < b * d

Only assumes left strict covariance.

theorem left.add_lt_add {α : Type u_1} [has_add α] [preorder α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c d : α} (h₁ : a < b) (h₂ : c < d) :
a + c < b + d

Only assumes left strict covariance

theorem right.add_lt_add {α : Type u_1} [has_add α] [preorder α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c d : α} (h₁ : a < b) (h₂ : c < d) :
a + c < b + d

Only assumes right strict covariance

theorem right.mul_lt_mul {α : Type u_1} [has_mul α] [preorder α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c d : α} (h₁ : a < b) (h₂ : c < d) :
a * c < b * d

Only assumes right strict covariance.

theorem add_le_add {α : Type u_1} [has_add α] [preorder α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c d : α} (h₁ : a b) (h₂ : c d) :
a + c b + d
theorem mul_le_mul' {α : Type u_1} [has_mul α] [preorder α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c d : α} (h₁ : a b) (h₂ : c d) :
a * c b * d
theorem mul_le_mul_three {α : Type u_1} [has_mul α] [preorder α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c d e f : α} (h₁ : a d) (h₂ : b e) (h₃ : c f) :
a * b * c d * e * f
theorem add_le_add_three {α : Type u_1} [has_add α] [preorder α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c d e f : α} (h₁ : a d) (h₂ : b e) (h₃ : c f) :
a + b + c d + e + f
theorem mul_lt_of_mul_lt_left {α : Type u_1} [has_mul α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b c d : α} (h : a * b < c) (hle : d b) :
a * d < c
theorem add_lt_of_add_lt_left {α : Type u_1} [has_add α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b c d : α} (h : a + b < c) (hle : d b) :
a + d < c
theorem add_le_of_add_le_left {α : Type u_1} [has_add α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b c d : α} (h : a + b c) (hle : d b) :
a + d c
theorem mul_le_of_mul_le_left {α : Type u_1} [has_mul α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b c d : α} (h : a * b c) (hle : d b) :
a * d c
theorem mul_lt_of_mul_lt_right {α : Type u_1} [has_mul α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c d : α} (h : a * b < c) (hle : d a) :
d * b < c
theorem add_lt_of_add_lt_right {α : Type u_1} [has_add α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c d : α} (h : a + b < c) (hle : d a) :
d + b < c
theorem mul_le_of_mul_le_right {α : Type u_1} [has_mul α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c d : α} (h : a * b c) (hle : d a) :
d * b c
theorem add_le_of_add_le_right {α : Type u_1} [has_add α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c d : α} (h : a + b c) (hle : d a) :
d + b c
theorem lt_add_of_lt_add_left {α : Type u_1} [has_add α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b c d : α} (h : a < b + c) (hle : c d) :
a < b + d
theorem lt_mul_of_lt_mul_left {α : Type u_1} [has_mul α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b c d : α} (h : a < b * c) (hle : c d) :
a < b * d
theorem le_add_of_le_add_left {α : Type u_1} [has_add α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b c d : α} (h : a b + c) (hle : c d) :
a b + d
theorem le_mul_of_le_mul_left {α : Type u_1} [has_mul α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b c d : α} (h : a b * c) (hle : c d) :
a b * d
theorem lt_add_of_lt_add_right {α : Type u_1} [has_add α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c d : α} (h : a < b + c) (hle : b d) :
a < d + c
theorem lt_mul_of_lt_mul_right {α : Type u_1} [has_mul α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c d : α} (h : a < b * c) (hle : b d) :
a < d * c
theorem le_mul_of_le_mul_right {α : Type u_1} [has_mul α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c d : α} (h : a b * c) (hle : b d) :
a d * c
theorem le_add_of_le_add_right {α : Type u_1} [has_add α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c d : α} (h : a b + c) (hle : b d) :
a d + c
theorem add_left_cancel'' {α : Type u_1} [has_add α] [partial_order α] [contravariant_class α α has_add.add has_le.le] {a b c : α} (h : a + b = a + c) :
b = c
theorem mul_left_cancel'' {α : Type u_1} [has_mul α] [partial_order α] [contravariant_class α α has_mul.mul has_le.le] {a b c : α} (h : a * b = a * c) :
b = c
theorem add_right_cancel'' {α : Type u_1} [has_add α] [partial_order α] [contravariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} (h : a + b = c + b) :
a = c
theorem mul_right_cancel'' {α : Type u_1} [has_mul α] [partial_order α] [contravariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} (h : a * b = c * b) :
a = c
theorem le_add_of_nonneg_right {α : Type u_1} [add_zero_class α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b : α} (h : 0 b) :
a a + b
theorem le_mul_of_one_le_right' {α : Type u_1} [mul_one_class α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (h : 1 b) :
a a * b
theorem mul_le_of_le_one_right' {α : Type u_1} [mul_one_class α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (h : b 1) :
a * b a
theorem add_le_of_nonpos_right {α : Type u_1} [add_zero_class α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b : α} (h : b 0) :
a + b a
theorem le_mul_of_one_le_left' {α : Type u_1} [mul_one_class α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} (h : 1 b) :
a b * a
theorem le_add_of_nonneg_left {α : Type u_1} [add_zero_class α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} (h : 0 b) :
a b + a
theorem add_le_of_nonpos_left {α : Type u_1} [add_zero_class α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} (h : b 0) :
b + a a
theorem mul_le_of_le_one_left' {α : Type u_1} [mul_one_class α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} (h : b 1) :
b * a a
@[simp]
theorem le_add_iff_nonneg_right {α : Type u_1} [add_zero_class α] [has_le α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_le.le] (a : α) {b : α} :
a a + b 0 b
@[simp]
theorem le_mul_iff_one_le_right' {α : Type u_1} [mul_one_class α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [contravariant_class α α has_mul.mul has_le.le] (a : α) {b : α} :
a a * b 1 b
@[simp]
@[simp]
@[simp]
theorem add_le_iff_nonpos_right {α : Type u_1} [add_zero_class α] [has_le α] [covariant_class α α has_add.add has_le.le] [contravariant_class α α has_add.add has_le.le] (a : α) {b : α} :
a + b a b 0
@[simp]
theorem mul_le_iff_le_one_right' {α : Type u_1} [mul_one_class α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [contravariant_class α α has_mul.mul has_le.le] (a : α) {b : α} :
a * b a b 1
theorem lt_add_of_pos_right {α : Type u_1} [add_zero_class α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] (a : α) {b : α} (h : 0 < b) :
a < a + b
theorem lt_mul_of_one_lt_right' {α : Type u_1} [mul_one_class α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] (a : α) {b : α} (h : 1 < b) :
a < a * b
theorem add_lt_of_neg_right {α : Type u_1} [add_zero_class α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] (a : α) {b : α} (h : b < 0) :
a + b < a
theorem mul_lt_of_lt_one_right' {α : Type u_1} [mul_one_class α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] (a : α) {b : α} (h : b < 1) :
a * b < a
theorem lt_add_of_pos_left {α : Type u_1} [add_zero_class α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] (a : α) {b : α} (h : 0 < b) :
a < b + a
theorem lt_mul_of_one_lt_left' {α : Type u_1} [mul_one_class α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (a : α) {b : α} (h : 1 < b) :
a < b * a
theorem add_lt_of_neg_left {α : Type u_1} [add_zero_class α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] (a : α) {b : α} (h : b < 0) :
b + a < a
theorem mul_lt_of_lt_one_left' {α : Type u_1} [mul_one_class α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (a : α) {b : α} (h : b < 1) :
b * a < a
@[simp]
theorem lt_add_iff_pos_right {α : Type u_1} [add_zero_class α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [contravariant_class α α has_add.add has_lt.lt] (a : α) {b : α} :
a < a + b 0 < b
@[simp]
theorem lt_mul_iff_one_lt_right' {α : Type u_1} [mul_one_class α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [contravariant_class α α has_mul.mul has_lt.lt] (a : α) {b : α} :
a < a * b 1 < b
@[simp]
theorem lt_add_iff_pos_left {α : Type u_1} [add_zero_class α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] [contravariant_class α α (function.swap has_add.add) has_lt.lt] (a : α) {b : α} :
a < b + a 0 < b
@[simp]
theorem lt_mul_iff_one_lt_left' {α : Type u_1} [mul_one_class α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] [contravariant_class α α (function.swap has_mul.mul) has_lt.lt] (a : α) {b : α} :
a < b * a 1 < b
@[simp]
theorem add_lt_iff_neg_left {α : Type u_1} [add_zero_class α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [contravariant_class α α has_add.add has_lt.lt] {a b : α} :
a + b < a b < 0
@[simp]
theorem mul_lt_iff_lt_one_left' {α : Type u_1} [mul_one_class α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [contravariant_class α α has_mul.mul has_lt.lt] {a b : α} :
a * b < a b < 1
@[simp]
theorem add_lt_iff_neg_right {α : Type u_1} [add_zero_class α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] [contravariant_class α α (function.swap has_add.add) has_lt.lt] {a : α} (b : α) :
a + b < b a < 0
@[simp]
theorem mul_lt_iff_lt_one_right' {α : Type u_1} [mul_one_class α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] [contravariant_class α α (function.swap has_mul.mul) has_lt.lt] {a : α} (b : α) :
a * b < b a < 1

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

theorem mul_le_of_le_of_le_one {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} (hbc : b c) (ha : a 1) :
b * a c
theorem add_le_of_le_of_nonpos {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b c : α} (hbc : b c) (ha : a 0) :
b + a c
theorem add_lt_of_le_of_neg {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} (hbc : b c) (ha : a < 0) :
b + a < c
theorem mul_lt_of_le_of_lt_one {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} (hbc : b c) (ha : a < 1) :
b * a < c
theorem add_lt_of_lt_of_nonpos {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b c : α} (hbc : b < c) (ha : a 0) :
b + a < c
theorem mul_lt_of_lt_of_le_one {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} (hbc : b < c) (ha : a 1) :
b * a < c
theorem mul_lt_of_lt_of_lt_one {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} (hbc : b < c) (ha : a < 1) :
b * a < c
theorem add_lt_of_lt_of_neg {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} (hbc : b < c) (ha : a < 0) :
b + a < c
theorem mul_lt_of_lt_of_lt_one' {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} (hbc : b < c) (ha : a < 1) :
b * a < c
theorem add_lt_of_lt_of_neg' {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b c : α} (hbc : b < c) (ha : a < 0) :
b + a < c
theorem left.add_nonpos {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b : α} (ha : a 0) (hb : b 0) :
a + b 0

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

theorem left.mul_le_one {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (ha : a 1) (hb : b 1) :
a * b 1

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

theorem left.mul_lt_one_of_le_of_lt {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] {a b : α} (ha : a 1) (hb : b < 1) :
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_nonpos_of_neg {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a b : α} (ha : a 0) (hb : b < 0) :
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_lt_of_le {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (ha : a < 1) (hb : b 1) :
a * b < 1

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

theorem left.add_neg_of_neg_of_nonpos {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b : α} (ha : a < 0) (hb : b 0) :
a + b < 0

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

theorem left.mul_lt_one {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] {a b : α} (ha : a < 1) (hb : b < 1) :
a * b < 1

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

theorem left.add_neg {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a b : α} (ha : a < 0) (hb : b < 0) :
a + b < 0

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

theorem left.mul_lt_one' {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (ha : a < 1) (hb : b < 1) :
a * b < 1

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

theorem left.add_neg' {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b : α} (ha : a < 0) (hb : b < 0) :
a + b < 0

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

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

theorem le_add_of_le_of_nonneg {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b c : α} (hbc : b c) (ha : 0 a) :
b c + a
theorem le_mul_of_le_of_one_le {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} (hbc : b c) (ha : 1 a) :
b c * a
theorem lt_add_of_le_of_pos {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} (hbc : b c) (ha : 0 < a) :
b < c + a
theorem lt_mul_of_le_of_one_lt {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} (hbc : b c) (ha : 1 < a) :
b < c * a
theorem lt_mul_of_lt_of_one_le {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} (hbc : b < c) (ha : 1 a) :
b < c * a
theorem lt_add_of_lt_of_nonneg {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b c : α} (hbc : b < c) (ha : 0 a) :
b < c + a
theorem lt_mul_of_lt_of_one_lt {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} (hbc : b < c) (ha : 1 < a) :
b < c * a
theorem lt_add_of_lt_of_pos {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} (hbc : b < c) (ha : 0 < a) :
b < c + a
theorem lt_add_of_lt_of_pos' {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b c : α} (hbc : b < c) (ha : 0 < a) :
b < c + a
theorem lt_mul_of_lt_of_one_lt' {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} (hbc : b < c) (ha : 1 < a) :
b < c * a
theorem left.one_le_mul {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (ha : 1 a) (hb : 1 b) :
1 a * b

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

theorem left.add_nonneg {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b : α} (ha : 0 a) (hb : 0 b) :
0 a + b

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

theorem left.add_pos_of_nonneg_of_pos {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a b : α} (ha : 0 a) (hb : 0 < b) :
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} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] {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} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {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} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {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.one_lt_mul {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] {a b : α} (ha : 1 < a) (hb : 1 < b) :
1 < a * b

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

theorem left.add_pos {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a b : α} (ha : 0 < a) (hb : 0 < b) :
0 < a + b

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

theorem left.add_pos' {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b : α} (ha : 0 < a) (hb : 0 < b) :
0 < a + b

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

theorem left.one_lt_mul' {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (ha : 1 < a) (hb : 1 < b) :
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} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} (ha : a 0) (hbc : b c) :
a + b c
theorem mul_le_of_le_one_of_le {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} (ha : a 1) (hbc : b c) :
a * b c
theorem mul_lt_of_lt_one_of_le {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c : α} (ha : a < 1) (hbc : b c) :
a * b < c
theorem add_lt_of_neg_of_le {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} (ha : a < 0) (hbc : b c) :
a + b < c
theorem mul_lt_of_le_one_of_lt {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} (ha : a 1) (hb : b < c) :
a * b < c
theorem add_lt_of_nonpos_of_lt {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} (ha : a 0) (hb : b < c) :
a + b < c
theorem add_lt_of_neg_of_lt {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} (ha : a < 0) (hb : b < c) :
a + b < c
theorem mul_lt_of_lt_one_of_lt {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c : α} (ha : a < 1) (hb : b < c) :
a * b < c
theorem mul_lt_of_lt_one_of_lt' {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} (ha : a < 1) (hbc : b < c) :
a * b < c
theorem add_lt_of_neg_of_lt' {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} (ha : a < 0) (hbc : b < c) :
a + b < c
theorem right.mul_le_one {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} (ha : a 1) (hb : b 1) :
a * b 1

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

theorem right.add_nonpos {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} (ha : a 0) (hb : b 0) :
a + b 0

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

theorem right.add_neg_of_neg_of_nonpos {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} (ha : a < 0) (hb : b 0) :
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} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {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.mul_lt_one_of_le_of_lt {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} (ha : a 1) (hb : b < 1) :
a * b < 1

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

theorem right.add_neg_of_nonpos_of_neg {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} (ha : a 0) (hb : b < 0) :
a + b < 0

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

theorem right.add_neg {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} (ha : a < 0) (hb : b < 0) :
a + b < 0

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

theorem right.mul_lt_one {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} (ha : a < 1) (hb : b < 1) :
a * b < 1

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

theorem right.add_neg' {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} (ha : a < 0) (hb : b < 0) :
a + b < 0

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

theorem right.mul_lt_one' {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} (ha : a < 1) (hb : b < 1) :
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} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} (ha : 0 a) (hbc : b c) :
b a + c
theorem le_mul_of_one_le_of_le {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} (ha : 1 a) (hbc : b c) :
b a * c
theorem lt_add_of_pos_of_le {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} (ha : 0 < a) (hbc : b c) :
b < a + c
theorem lt_mul_of_one_lt_of_le {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c : α} (ha : 1 < a) (hbc : b c) :
b < a * c
theorem lt_mul_of_one_le_of_lt {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} (ha : 1 a) (hbc : b < c) :
b < a * c
theorem lt_add_of_nonneg_of_lt {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} (ha : 0 a) (hbc : b < c) :
b < a + c
theorem lt_mul_of_one_lt_of_lt {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c : α} (ha : 1 < a) (hbc : b < c) :
b < a * c
theorem lt_add_of_pos_of_lt {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} (ha : 0 < a) (hbc : b < c) :
b < a + c
theorem lt_add_of_pos_of_lt' {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} (ha : 0 < a) (hbc : b < c) :
b < a + c
theorem lt_mul_of_one_lt_of_lt' {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} (ha : 1 < a) (hbc : b < c) :
b < a * c
theorem right.add_nonneg {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} (ha : 0 a) (hb : 0 b) :
0 a + b

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

theorem right.one_le_mul {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} (ha : 1 a) (hb : 1 b) :
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} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {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} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {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} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {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} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {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} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {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} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {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} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {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} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {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} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (ha : a 1) (hb : b 1) :
a * b 1

Alias of left.mul_le_one.

theorem mul_lt_one_of_le_of_lt {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] {a b : α} (ha : a 1) (hb : b < 1) :
a * b < 1

Alias of left.mul_lt_one_of_le_of_lt.

theorem mul_lt_one_of_lt_of_le {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (ha : a < 1) (hb : b 1) :
a * b < 1

Alias of left.mul_lt_one_of_lt_of_le.

theorem mul_lt_one {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] {a b : α} (ha : a < 1) (hb : b < 1) :
a * b < 1

Alias of left.mul_lt_one.

theorem mul_lt_one' {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (ha : a < 1) (hb : b < 1) :
a * b < 1

Alias of left.mul_lt_one'.

theorem add_nonpos {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b : α} (ha : a 0) (hb : b 0) :
a + b 0

Alias of left.add_nonpos.

theorem add_neg_of_nonpos_of_neg {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a b : α} (ha : a 0) (hb : b < 0) :
a + b < 0

Alias of left.add_neg_of_nonpos_of_neg.

theorem add_neg_of_neg_of_nonpos {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b : α} (ha : a < 0) (hb : b 0) :
a + b < 0

Alias of left.add_neg_of_neg_of_nonpos.

theorem add_neg {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a b : α} (ha : a < 0) (hb : b < 0) :
a + b < 0

Alias of left.add_neg.

theorem add_neg' {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b : α} (ha : a < 0) (hb : b < 0) :
a + b < 0

Alias of left.add_neg'.

theorem one_le_mul {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (ha : 1 a) (hb : 1 b) :
1 a * b

Alias of left.one_le_mul.

theorem one_lt_mul_of_le_of_lt' {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] {a b : α} (ha : 1 a) (hb : 1 < b) :
1 < a * b

Alias of left.one_lt_mul_of_le_of_lt.

theorem one_lt_mul_of_lt_of_le' {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (ha : 1 < a) (hb : 1 b) :
1 < a * b

Alias of left.one_lt_mul_of_lt_of_le.

theorem one_lt_mul' {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] {a b : α} (ha : 1 < a) (hb : 1 < b) :
1 < a * b

Alias of left.one_lt_mul.

theorem one_lt_mul'' {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (ha : 1 < a) (hb : 1 < b) :
1 < a * b

Alias of left.one_lt_mul'.

theorem add_nonneg {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b : α} (ha : 0 a) (hb : 0 b) :
0 a + b

Alias of left.add_nonneg.

theorem add_pos_of_nonneg_of_pos {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a b : α} (ha : 0 a) (hb : 0 < b) :
0 < a + b

Alias of left.add_pos_of_nonneg_of_pos.

theorem add_pos_of_pos_of_nonneg {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b : α} (ha : 0 < a) (hb : 0 b) :
0 < a + b

Alias of left.add_pos_of_pos_of_nonneg.

theorem add_pos {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a b : α} (ha : 0 < a) (hb : 0 < b) :
0 < a + b

Alias of left.add_pos.

theorem add_pos' {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b : α} (ha : 0 < a) (hb : 0 < b) :
0 < a + b

Alias of left.add_pos'.

theorem lt_of_mul_lt_of_one_le_left {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} (h : a * b < c) (hle : 1 b) :
a < c
theorem lt_of_add_lt_of_nonneg_left {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b c : α} (h : a + b < c) (hle : 0 b) :
a < c
theorem le_of_mul_le_of_one_le_left {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} (h : a * b c) (hle : 1 b) :
a c
theorem le_of_add_le_of_nonneg_left {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b c : α} (h : a + b c) (hle : 0 b) :
a c
theorem lt_of_lt_add_of_nonpos_left {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b c : α} (h : a < b + c) (hle : c 0) :
a < b
theorem lt_of_lt_mul_of_le_one_left {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} (h : a < b * c) (hle : c 1) :
a < b
theorem le_of_le_add_of_nonpos_left {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b c : α} (h : a b + c) (hle : c 0) :
a b
theorem le_of_le_mul_of_le_one_left {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} (h : a b * c) (hle : c 1) :
a b
theorem lt_of_mul_lt_of_one_le_right {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} (h : a * b < c) (hle : 1 a) :
b < c
theorem lt_of_add_lt_of_nonneg_right {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} (h : a + b < c) (hle : 0 a) :
b < c
theorem le_of_mul_le_of_one_le_right {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} (h : a * b c) (hle : 1 a) :
b c
theorem le_of_add_le_of_nonneg_right {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} (h : a + b c) (hle : 0 a) :
b c
theorem lt_of_lt_add_of_nonpos_right {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} (h : a < b + c) (hle : b 0) :
a < c
theorem lt_of_lt_mul_of_le_one_right {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} (h : a < b * c) (hle : b 1) :
a < c
theorem le_of_le_mul_of_le_one_right {α : Type u_1} [mul_one_class α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} (h : a b * c) (hle : b 1) :
a c
theorem le_of_le_add_of_nonpos_right {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} (h : a b + c) (hle : b 0) :
a c
theorem add_eq_zero_iff' {α : Type u_1} [add_zero_class α] [partial_order α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} (ha : 0 a) (hb : 0 b) :
a + b = 0 a = 0 b = 0
theorem mul_eq_one_iff' {α : Type u_1} [mul_one_class α] [partial_order α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} (ha : 1 a) (hb : 1 b) :
a * b = 1 a = 1 b = 1
theorem eq_zero_of_add_nonneg_left {α : Type u_1} [add_zero_class α] [partial_order α] [covariant_class α α has_add.add has_le.le] {a b : α} (ha : a 0) (hb : b 0) (hab : 0 a + b) :
a = 0
theorem eq_one_of_one_le_mul_left {α : Type u_1} [mul_one_class α] [partial_order α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (ha : a 1) (hb : b 1) (hab : 1 a * b) :
a = 1
theorem eq_one_of_mul_le_one_left {α : Type u_1} [mul_one_class α] [partial_order α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (ha : 1 a) (hb : 1 b) (hab : a * b 1) :
a = 1
theorem eq_zero_of_add_nonpos_left {α : Type u_1} [add_zero_class α] [partial_order α] [covariant_class α α has_add.add has_le.le] {a b : α} (ha : 0 a) (hb : 0 b) (hab : a + b 0) :
a = 0
theorem eq_one_of_one_le_mul_right {α : Type u_1} [mul_one_class α] [partial_order α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} (ha : a 1) (hb : b 1) (hab : 1 a * b) :
b = 1
theorem eq_zero_of_add_nonneg_right {α : Type u_1} [add_zero_class α] [partial_order α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} (ha : a 0) (hb : b 0) (hab : 0 a + b) :
b = 0
theorem eq_one_of_mul_le_one_right {α : Type u_1} [mul_one_class α] [partial_order α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} (ha : 1 a) (hb : 1 b) (hab : a * b 1) :
b = 1
theorem eq_zero_of_add_nonpos_right {α : Type u_1} [add_zero_class α] [partial_order α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} (ha : 0 a) (hb : 0 b) (hab : a + b 0) :
b = 0
theorem exists_square_le {α : Type u_1} [mul_one_class α] [linear_order α] [covariant_class α α has_mul.mul has_lt.lt] (a : α) :
∃ (b : α), b * b a

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

Equations

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

Equations

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

Equations

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

Equations
theorem monotone.const_add {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f : β → α} [covariant_class α α has_add.add has_le.le] (hf : monotone f) (a : α) :
monotone (λ (x : β), a + f x)
theorem monotone.const_mul' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f : β → α} [covariant_class α α has_mul.mul has_le.le] (hf : monotone f) (a : α) :
monotone (λ (x : β), a * f x)
theorem monotone_on.const_add {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f : β → α} {s : set β} [covariant_class α α has_add.add has_le.le] (hf : monotone_on f s) (a : α) :
monotone_on (λ (x : β), a + f x) s
theorem monotone_on.const_mul' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f : β → α} {s : set β} [covariant_class α α has_mul.mul has_le.le] (hf : monotone_on f s) (a : α) :
monotone_on (λ (x : β), a * f x) s
theorem antitone.const_add {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f : β → α} [covariant_class α α has_add.add has_le.le] (hf : antitone f) (a : α) :
antitone (λ (x : β), a + f x)
theorem antitone.const_mul' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f : β → α} [covariant_class α α has_mul.mul has_le.le] (hf : antitone f) (a : α) :
antitone (λ (x : β), a * f x)
theorem antitone_on.const_mul' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f : β → α} {s : set β} [covariant_class α α has_mul.mul has_le.le] (hf : antitone_on f s) (a : α) :
antitone_on (λ (x : β), a * f x) s
theorem antitone_on.const_add {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f : β → α} {s : set β} [covariant_class α α has_add.add has_le.le] (hf : antitone_on f s) (a : α) :
antitone_on (λ (x : β), a + f x) s
theorem monotone.add_const {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f : β → α} [covariant_class α α (function.swap has_add.add) has_le.le] (hf : monotone f) (a : α) :
monotone (λ (x : β), f x + a)
theorem monotone.mul_const' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f : β → α} [covariant_class α α (function.swap has_mul.mul) has_le.le] (hf : monotone f) (a : α) :
monotone (λ (x : β), f x * a)
theorem monotone_on.mul_const' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f : β → α} {s : set β} [covariant_class α α (function.swap has_mul.mul) has_le.le] (hf : monotone_on f s) (a : α) :
monotone_on (λ (x : β), f x * a) s
theorem monotone_on.add_const {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f : β → α} {s : set β} [covariant_class α α (function.swap has_add.add) has_le.le] (hf : monotone_on f s) (a : α) :
monotone_on (λ (x : β), f x + a) s
theorem antitone.mul_const' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f : β → α} [covariant_class α α (function.swap has_mul.mul) has_le.le] (hf : antitone f) (a : α) :
antitone (λ (x : β), f x * a)
theorem antitone.add_const {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f : β → α} [covariant_class α α (function.swap has_add.add) has_le.le] (hf : antitone f) (a : α) :
antitone (λ (x : β), f x + a)
theorem antitone_on.mul_const' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f : β → α} {s : set β} [covariant_class α α (function.swap has_mul.mul) has_le.le] (hf : antitone_on f s) (a : α) :
antitone_on (λ (x : β), f x * a) s
theorem antitone_on.add_const {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f : β → α} {s : set β} [covariant_class α α (function.swap has_add.add) has_le.le] (hf : antitone_on f s) (a : α) :
antitone_on (λ (x : β), f x + a) s
theorem monotone.mul' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f g : β → α} [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (hf : monotone f) (hg : monotone g) :
monotone (λ (x : β), f x * g x)

The product of two monotone functions is monotone.

theorem monotone.add {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f g : β → α} [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (hf : monotone f) (hg : monotone g) :
monotone (λ (x : β), f x + g x)

The sum of two monotone functions is monotone.

theorem monotone_on.mul' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f g : β → α} {s : set β} [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (hf : monotone_on f s) (hg : monotone_on g s) :
monotone_on (λ (x : β), f x * g x) s

The product of two monotone functions is monotone.

theorem monotone_on.add {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f g : β → α} {s : set β} [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (hf : monotone_on f s) (hg : monotone_on g s) :
monotone_on (λ (x : β), f x + g x) s

The sum of two monotone functions is monotone.

theorem antitone.add {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f g : β → α} [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (hf : antitone f) (hg : antitone g) :
antitone (λ (x : β), f x + g x)

The sum of two antitone functions is antitone.

theorem antitone.mul' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f g : β → α} [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (hf : antitone f) (hg : antitone g) :
antitone (λ (x : β), f x * g x)

The product of two antitone functions is antitone.

theorem antitone_on.mul' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f g : β → α} {s : set β} [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (hf : antitone_on f s) (hg : antitone_on g s) :
antitone_on (λ (x : β), f x * g x) s

The product of two antitone functions is antitone.

theorem antitone_on.add {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f g : β → α} {s : set β} [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (hf : antitone_on f s) (hg : antitone_on g s) :
antitone_on (λ (x : β), f x + g x) s

The sum of two antitone functions is antitone.

theorem strict_mono.const_add {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f : β → α} [covariant_class α α has_add.add has_lt.lt] (hf : strict_mono f) (c : α) :
strict_mono (λ (x : β), c + f x)
theorem strict_mono.const_mul' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f : β → α} [covariant_class α α has_mul.mul has_lt.lt] (hf : strict_mono f) (c : α) :
strict_mono (λ (x : β), c * f x)
theorem strict_mono_on.const_mul' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f : β → α} {s : set β} [covariant_class α α has_mul.mul has_lt.lt] (hf : strict_mono_on f s) (c : α) :
strict_mono_on (λ (x : β), c * f x) s
theorem strict_mono_on.const_add {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f : β → α} {s : set β} [covariant_class α α has_add.add has_lt.lt] (hf : strict_mono_on f s) (c : α) :
strict_mono_on (λ (x : β), c + f x) s
theorem strict_anti.const_add {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f : β → α} [covariant_class α α has_add.add has_lt.lt] (hf : strict_anti f) (c : α) :
strict_anti (λ (x : β), c + f x)
theorem strict_anti.const_mul' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f : β → α} [covariant_class α α has_mul.mul has_lt.lt] (hf : strict_anti f) (c : α) :
strict_anti (λ (x : β), c * f x)
theorem strict_anti_on.const_add {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f : β → α} {s : set β} [covariant_class α α has_add.add has_lt.lt] (hf : strict_anti_on f s) (c : α) :
strict_anti_on (λ (x : β), c + f x) s
theorem strict_anti_on.const_mul' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f : β → α} {s : set β} [covariant_class α α has_mul.mul has_lt.lt] (hf : strict_anti_on f s) (c : α) :
strict_anti_on (λ (x : β), c * f x) s
theorem strict_mono.add_const {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f : β → α} [covariant_class α α (function.swap has_add.add) has_lt.lt] (hf : strict_mono f) (c : α) :
strict_mono (λ (x : β), f x + c)
theorem strict_mono.mul_const' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f : β → α} [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (hf : strict_mono f) (c : α) :
strict_mono (λ (x : β), f x * c)
theorem strict_mono_on.add_const {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f : β → α} {s : set β} [covariant_class α α (function.swap has_add.add) has_lt.lt] (hf : strict_mono_on f s) (c : α) :
strict_mono_on (λ (x : β), f x + c) s
theorem strict_mono_on.mul_const' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f : β → α} {s : set β} [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (hf : strict_mono_on f s) (c : α) :
strict_mono_on (λ (x : β), f x * c) s
theorem strict_anti.mul_const' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f : β → α} [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (hf : strict_anti f) (c : α) :
strict_anti (λ (x : β), f x * c)
theorem strict_anti.add_const {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f : β → α} [covariant_class α α (function.swap has_add.add) has_lt.lt] (hf : strict_anti f) (c : α) :
strict_anti (λ (x : β), f x + c)
theorem strict_anti_on.add_const {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f : β → α} {s : set β} [covariant_class α α (function.swap has_add.add) has_lt.lt] (hf : strict_anti_on f s) (c : α) :
strict_anti_on (λ (x : β), f x + c) s
theorem strict_anti_on.mul_const' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f : β → α} {s : set β} [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (hf : strict_anti_on f s) (c : α) :
strict_anti_on (λ (x : β), f x * c) s
theorem strict_mono.mul' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f g : β → α} [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (hf : strict_mono f) (hg : strict_mono g) :
strict_mono (λ (x : β), f x * g x)

The product of two strictly monotone functions is strictly monotone.

theorem strict_mono.add {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f g : β → α} [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] (hf : strict_mono f) (hg : strict_mono g) :
strict_mono (λ (x : β), f x + g x)

The sum of two strictly monotone functions is strictly monotone.

theorem strict_mono_on.mul' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f g : β → α} {s : set β} [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (hf : strict_mono_on f s) (hg : strict_mono_on g s) :
strict_mono_on (λ (x : β), f x * g x) s

The product of two strictly monotone functions is strictly monotone.

theorem strict_mono_on.add {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f g : β → α} {s : set β} [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] (hf : strict_mono_on f s) (hg : strict_mono_on g s) :
strict_mono_on (λ (x : β), f x + g x) s

The sum of two strictly monotone functions is strictly monotone.

theorem strict_anti.add {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f g : β → α} [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] (hf : strict_anti f) (hg : strict_anti g) :
strict_anti (λ (x : β), f x + g x)

The sum of two strictly antitone functions is strictly antitone.

theorem strict_anti.mul' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f g : β → α} [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (hf : strict_anti f) (hg : strict_anti g) :
strict_anti (λ (x : β), f x * g x)

The product of two strictly antitone functions is strictly antitone.

theorem strict_anti_on.mul' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f g : β → α} {s : set β} [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (hf : strict_anti_on f s) (hg : strict_anti_on g s) :
strict_anti_on (λ (x : β), f x * g x) s

The product of two strictly antitone functions is strictly antitone.

theorem strict_anti_on.add {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f g : β → α} {s : set β} [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] (hf : strict_anti_on f s) (hg : strict_anti_on g s) :
strict_anti_on (λ (x : β), f x + g x) s

The sum of two strictly antitone functions is strictly antitone.

theorem monotone.mul_strict_mono' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_le.le] {f g : β → α} (hf : monotone f) (hg : strict_mono g) :
strict_mono (λ (x : β), f x * g x)

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

theorem monotone.add_strict_mono {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_le.le] {f g : β → α} (hf : monotone f) (hg : strict_mono g) :
strict_mono (λ (x : β), f x + g x)

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

theorem monotone_on.add_strict_mono {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {s : set β} [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_le.le] {f g : β → α} (hf : monotone_on f s) (hg : strict_mono_on g s) :
strict_mono_on (λ (x : β), f x + g x) s

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

theorem monotone_on.mul_strict_mono' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {s : set β} [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_le.le] {f g : β → α} (hf : monotone_on f s) (hg : strict_mono_on g s) :
strict_mono_on (λ (x : β), f x * g x) s

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

theorem antitone.mul_strict_anti' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_le.le] {f g : β → α} (hf : antitone f) (hg : strict_anti g) :
strict_anti (λ (x : β), f x * g x)

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

theorem antitone.add_strict_anti {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_le.le] {f g : β → α} (hf : antitone f) (hg : strict_anti g) :
strict_anti (λ (x : β), f x + g x)

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

theorem antitone_on.mul_strict_anti' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {s : set β} [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_le.le] {f g : β → α} (hf : antitone_on f s) (hg : strict_anti_on g s) :
strict_anti_on (λ (x : β), f x * g x) s

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

theorem antitone_on.add_strict_anti {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {s : set β} [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_le.le] {f g : β → α} (hf : antitone_on f s) (hg : strict_anti_on g s) :
strict_anti_on (λ (x : β), f x + g x) s

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

theorem strict_mono.add_monotone {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f g : β → α} [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_lt.lt] (hf : strict_mono f) (hg : monotone g) :
strict_mono (λ (x : β), f x + g x)

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

theorem strict_mono.mul_monotone' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f g : β → α} [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (hf : strict_mono f) (hg : monotone g) :
strict_mono (λ (x : β), f x * g x)

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

theorem strict_mono_on.add_monotone {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f g : β → α} {s : set β} [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_lt.lt] (hf : strict_mono_on f s) (hg : monotone_on g s) :
strict_mono_on (λ (x : β), f x + g x) s

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

theorem strict_mono_on.mul_monotone' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f g : β → α} {s : set β} [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (hf : strict_mono_on f s) (hg : monotone_on g s) :
strict_mono_on (λ (x : β), f x * g x) s

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

theorem strict_anti.mul_antitone' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f g : β → α} [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (hf : strict_anti f) (hg : antitone g) :
strict_anti (λ (x : β), f x * g x)

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

theorem strict_anti.add_antitone {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f g : β → α} [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_lt.lt] (hf : strict_anti f) (hg : antitone g) :
strict_anti (λ (x : β), f x + g x)

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

theorem strict_anti_on.add_antitone {α : Type u_1} {β : Type u_2} [has_add α] [preorder α] [preorder β] {f g : β → α} {s : set β} [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_lt.lt] (hf : strict_anti_on f s) (hg : antitone_on g s) :
strict_anti_on (λ (x : β), f x + g x) s

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

theorem strict_anti_on.mul_antitone' {α : Type u_1} {β : Type u_2} [has_mul α] [preorder α] [preorder β] {f g : β → α} {s : set β} [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (hf : strict_anti_on f s) (hg : antitone_on g s) :
strict_anti_on (λ (x : β), f x * g x) s

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

@[simp]
theorem cmp_add_left {α : Type u_1} [has_add α] [linear_order α] [covariant_class α α has_add.add has_lt.lt] (a b c : α) :
cmp (a + b) (a + c) = cmp b c
@[simp]
theorem cmp_mul_left' {α : Type u_1} [has_mul α] [linear_order α] [covariant_class α α has_mul.mul has_lt.lt] (a b c : α) :
cmp (a * b) (a * c) = cmp b c
@[simp]
theorem cmp_mul_right' {α : Type u_1} [has_mul α] [linear_order α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (a b c : α) :
cmp (a * c) (b * c) = cmp a b
@[simp]
theorem cmp_add_right {α : Type u_1} [has_add α] [linear_order α] [covariant_class α α (function.swap has_add.add) has_lt.lt] (a b c : α) :
cmp (a + c) (b + c) = cmp a b
def add_le_cancellable {α : Type u_1} [has_add α] [has_le α] (a : α) :
Prop

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

Equations
def mul_le_cancellable {α : Type u_1} [has_mul α] [has_le α] (a : α) :
Prop

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

Equations
theorem mul_le_cancellable_one {α : Type u_1} [monoid α] [has_le α] :
theorem add_le_cancellable_zero {α : Type u_1} [add_monoid α] [has_le α] :
@[protected]
theorem mul_le_cancellable.injective {α : Type u_1} [has_mul α] [partial_order α] {a : α} (ha : mul_le_cancellable a) :
@[protected]
theorem add_le_cancellable.injective {α : Type u_1} [has_add α] [partial_order α] {a : α} (ha : add_le_cancellable a) :
@[protected]
theorem mul_le_cancellable.inj {α : Type u_1} [has_mul α] [partial_order α] {a b c : α} (ha : mul_le_cancellable a) :
a * b = a * c b = c
@[protected]
theorem add_le_cancellable.inj {α : Type u_1} [has_add α] [partial_order α] {a b c : α} (ha : add_le_cancellable a) :
a + b = a + c b = c
@[protected]
theorem add_le_cancellable.injective_left {α : Type u_1} [add_comm_semigroup α] [partial_order α] {a : α} (ha : add_le_cancellable a) :
function.injective (λ (_x : α), _x + a)
@[protected]
theorem mul_le_cancellable.injective_left {α : Type u_1} [comm_semigroup α] [partial_order α] {a : α} (ha : mul_le_cancellable a) :
function.injective (λ (_x : α), _x * a)
@[protected]
theorem add_le_cancellable.inj_left {α : Type u_1} [add_comm_semigroup α] [partial_order α] {a b c : α} (hc : add_le_cancellable c) :
a + c = b + c a = b
@[protected]
theorem mul_le_cancellable.inj_left {α : Type u_1} [comm_semigroup α] [partial_order α] {a b c : α} (hc : mul_le_cancellable c) :
a * c = b * c a = b
@[protected]
theorem mul_le_cancellable.mul_le_mul_iff_left {α : Type u_1} [has_le α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} (ha : mul_le_cancellable a) :
a * b a * c b c
@[protected]
theorem add_le_cancellable.add_le_add_iff_left {α : Type u_1} [has_le α] [has_add α] [covariant_class α α has_add.add has_le.le] {a b c : α} (ha : add_le_cancellable a) :
a + b a + c b c
@[protected]
theorem mul_le_cancellable.mul_le_mul_iff_right {α : Type u_1} [has_le α] [comm_semigroup α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} (ha : mul_le_cancellable a) :
b * a c * a b c
@[protected]
theorem add_le_cancellable.add_le_add_iff_right {α : Type u_1} [has_le α] [add_comm_semigroup α] [covariant_class α α has_add.add has_le.le] {a b c : α} (ha : add_le_cancellable a) :
b + a c + a b c
@[protected]
theorem add_le_cancellable.le_add_iff_nonneg_right {α : Type u_1} [has_le α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] {a b : α} (ha : add_le_cancellable a) :
a a + b 0 b
@[protected]
theorem mul_le_cancellable.le_mul_iff_one_le_right {α : Type u_1} [has_le α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (ha : mul_le_cancellable a) :
a a * b 1 b
@[protected]
theorem mul_le_cancellable.mul_le_iff_le_one_right {α : Type u_1} [has_le α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (ha : mul_le_cancellable a) :
a * b a b 1
@[protected]
theorem add_le_cancellable.add_le_iff_nonpos_right {α : Type u_1} [has_le α] [add_zero_class α] [covariant_class α α has_add.add has_le.le] {a b : α} (ha : add_le_cancellable a) :
a + b a b 0
@[protected]
theorem add_le_cancellable.le_add_iff_nonneg_left {α : Type u_1} [has_le α] [add_comm_monoid α] [covariant_class α α has_add.add has_le.le] {a b : α} (ha : add_le_cancellable a) :
a b + a 0 b
@[protected]
theorem mul_le_cancellable.le_mul_iff_one_le_left {α : Type u_1} [has_le α] [comm_monoid α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (ha : mul_le_cancellable a) :
a b * a 1 b
@[protected]
theorem add_le_cancellable.add_le_iff_nonpos_left {α : Type u_1} [has_le α] [add_comm_monoid α] [covariant_class α α has_add.add has_le.le] {a b : α} (ha : add_le_cancellable a) :
b + a a b 0
@[protected]
theorem mul_le_cancellable.mul_le_iff_le_one_left {α : Type u_1} [has_le α] [comm_monoid α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (ha : mul_le_cancellable a) :
b * a a b 1