algebra.ordered_monoid - mathlib docs

source

@[instance]

def ordered_comm_monoid.to_comm_monoid (α : Type u_1) [s : ordered_comm_monoid α] :

comm_monoid α

source

@[instance]

def ordered_comm_monoid.to_partial_order (α : Type u_1) [s : ordered_comm_monoid α] :

partial_order α

source

@[class]

structure ordered_comm_monoid (α : Type u_1) :

Type u_1

mul : α → α → α
mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
mul_comm : ∀ (a b : α), a * b = b * a
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 * a ≤ c_1 * b
lt_of_mul_lt_mul_left : ∀ (a b c_1 : α), a * b < a * c_1 → b < c_1

An ordered commutative monoid is a commutative monoid with a partial order such that

a ≤ b → c * a ≤ c * b (multiplication is monotone)
a * b < a * c → b < c.

Instances

source

@[instance]

def ordered_add_comm_monoid.to_partial_order (α : Type u_1) [s : ordered_add_comm_monoid α] :

partial_order α

source

@[instance]

def ordered_add_comm_monoid.to_add_comm_monoid (α : Type u_1) [s : ordered_add_comm_monoid α] :

add_comm_monoid α

source

@[class]

structure ordered_add_comm_monoid (α : Type u_1) :

Type u_1

add : α → α → α
add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
add_comm : ∀ (a b : α), a + b = b + a
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b
lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1 → b < c_1

An ordered (additive) commutative monoid is a commutative monoid with a partial order such that

a ≤ b → c + a ≤ c + b (addition is monotone)
a + b < a + c → b < c.

Instances

source

@[class]

structure has_exists_mul_of_le (α : Type u) [ordered_comm_monoid α] :

Prop

exists_mul_of_le : ∀ {a b : α}, a ≤ b → (∃ (c : α), b = a * c)

An ordered_comm_monoid with one-sided 'division' in the sense that if a ≤ b, there is some c for which a * c = b. This is a weaker version of the condition on canonical orderings defined by canonically_ordered_monoid.

Instances

source

@[class]

structure has_exists_add_of_le (α : Type u) [ordered_add_comm_monoid α] :

Prop

exists_add_of_le : ∀ {a b : α}, a ≤ b → (∃ (c : α), b = a + c)

An ordered_add_comm_monoid with one-sided 'subtraction' in the sense that if a ≤ b, then there is some c for which a + c = b. This is a weaker version of the condition on canonical orderings defined by canonically_ordered_add_monoid.

Instances

source

@[instance]

def linear_ordered_add_comm_monoid.to_ordered_add_comm_monoid (α : Type u_1) [s : linear_ordered_add_comm_monoid α] :

ordered_add_comm_monoid α

source

@[instance]

def linear_ordered_add_comm_monoid.to_linear_order (α : Type u_1) [s : linear_ordered_add_comm_monoid α] :

linear_order α

source

@[class]

structure linear_ordered_add_comm_monoid (α : Type u_1) :

Type u_1

le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
decidable_le : decidable_rel has_le.le
decidable_eq : decidable_eq α
decidable_lt : decidable_rel has_lt.lt
add : α → α → α
add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
add_comm : ∀ (a b : α), a + b = b + a
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b
lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1 → b < c_1

A linearly ordered additive commutative monoid.

Instances

source

@[class]

structure linear_ordered_comm_monoid (α : Type u_1) :

Type u_1

le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
decidable_le : decidable_rel has_le.le
decidable_eq : decidable_eq α
decidable_lt : decidable_rel has_lt.lt
mul : α → α → α
mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
mul_comm : ∀ (a b : α), a * b = b * a
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 * a ≤ c_1 * b
lt_of_mul_lt_mul_left : ∀ (a b c_1 : α), a * b < a * c_1 → b < c_1

A linearly ordered commutative monoid.

Instances

source

@[instance]

def linear_ordered_comm_monoid.to_linear_order (α : Type u_1) [s : linear_ordered_comm_monoid α] :

linear_order α

source

@[instance]

def linear_ordered_comm_monoid.to_ordered_comm_monoid (α : Type u_1) [s : linear_ordered_comm_monoid α] :

ordered_comm_monoid α

source

@[instance]

def linear_ordered_comm_monoid_with_zero.to_comm_monoid_with_zero (α : Type u_1) [s : linear_ordered_comm_monoid_with_zero α] :

comm_monoid_with_zero α

source

@[class]

structure linear_ordered_comm_monoid_with_zero (α : Type u_1) :

Type u_1

le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
decidable_le : decidable_rel has_le.le
decidable_eq : decidable_eq α
decidable_lt : decidable_rel has_lt.lt
mul : α → α → α
mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
mul_comm : ∀ (a b : α), a * b = b * a
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 * a ≤ c_1 * b
lt_of_mul_lt_mul_left : ∀ (a b c_1 : α), a * b < a * c_1 → b < c_1
zero : α
zero_mul : ∀ (a : α), 0 * a = 0
mul_zero : ∀ (a : α), a * 0 = 0
zero_le_one : 0 ≤ 1

A linearly ordered commutative monoid with a zero element.

Instances

source

@[instance]

def linear_ordered_comm_monoid_with_zero.to_linear_ordered_comm_monoid (α : Type u_1) [s : linear_ordered_comm_monoid_with_zero α] :

linear_ordered_comm_monoid α

source

@[instance]

def linear_ordered_add_comm_monoid_with_top.to_linear_ordered_add_comm_monoid (α : Type u_1) [s : linear_ordered_add_comm_monoid_with_top α] :

linear_ordered_add_comm_monoid α

source

@[instance]

def linear_ordered_add_comm_monoid_with_top.to_order_top (α : Type u_1) [s : linear_ordered_add_comm_monoid_with_top α] :

order_top α

source

@[class]

structure linear_ordered_add_comm_monoid_with_top (α : Type u_1) :

Type u_1

le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
decidable_le : decidable_rel has_le.le
decidable_eq : decidable_eq α
decidable_lt : decidable_rel has_lt.lt
add : α → α → α
add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
add_comm : ∀ (a b : α), a + b = b + a
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b
lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1 → b < c_1
top : α
le_top : ∀ (a : α), a ≤ ⊤
top_add' : ∀ (x : α), ⊤ + x = ⊤

A linearly ordered commutative monoid with an additively absorbing ⊤ element. Instances should include number systems with an infinite element adjoined.`

Instances

source

@[simp]

theorem top_add {α : Type u} [linear_ordered_add_comm_monoid_with_top α] (a : α) :

⊤ + a = ⊤

source

@[simp]

theorem add_top {α : Type u} [linear_ordered_add_comm_monoid_with_top α] (a : α) :

a + ⊤ = ⊤

source

theorem mul_le_mul_left' {α : Type u} [ordered_comm_monoid α] {a b : α} (h : a ≤ b) (c : α) :

c * a ≤ c * b

source

theorem add_le_add_left {α : Type u} [ordered_add_comm_monoid α] {a b : α} (h : a ≤ b) (c : α) :

c + a ≤ c + b

source

theorem add_le_add_right {α : Type u} [ordered_add_comm_monoid α] {a b : α} (h : a ≤ b) (c : α) :

a + c ≤ b + c

source

theorem mul_le_mul_right' {α : Type u} [ordered_comm_monoid α] {a b : α} (h : a ≤ b) (c : α) :

a * c ≤ b * c

source

theorem mul_lt_of_mul_lt_left {α : Type u} [ordered_comm_monoid α] {a b c d : α} (h : a * b < c) (hle : d ≤ b) :

a * d < c

source

theorem add_lt_of_add_lt_left {α : Type u} [ordered_add_comm_monoid α] {a b c d : α} (h : a + b < c) (hle : d ≤ b) :

a + d < c

source

theorem mul_lt_of_mul_lt_right {α : Type u} [ordered_comm_monoid α] {a b c d : α} (h : a * b < c) (hle : d ≤ a) :

d * b < c

source

theorem add_lt_of_add_lt_right {α : Type u} [ordered_add_comm_monoid α] {a b c d : α} (h : a + b < c) (hle : d ≤ a) :

d + b < c

source

theorem add_le_of_add_le_left {α : Type u} [ordered_add_comm_monoid α] {a b c d : α} (h : a + b ≤ c) (hle : d ≤ b) :

a + d ≤ c

source

theorem mul_le_of_mul_le_left {α : Type u} [ordered_comm_monoid α] {a b c d : α} (h : a * b ≤ c) (hle : d ≤ b) :

a * d ≤ c

source

theorem mul_le_of_mul_le_right {α : Type u} [ordered_comm_monoid α] {a b c d : α} (h : a * b ≤ c) (hle : d ≤ a) :

d * b ≤ c

source

theorem add_le_of_add_le_right {α : Type u} [ordered_add_comm_monoid α] {a b c d : α} (h : a + b ≤ c) (hle : d ≤ a) :

d + b ≤ c

source

theorem lt_add_of_lt_add_left {α : Type u} [ordered_add_comm_monoid α] {a b c d : α} (h : a < b + c) (hle : c ≤ d) :

a < b + d

source

theorem lt_mul_of_lt_mul_left {α : Type u} [ordered_comm_monoid α] {a b c d : α} (h : a < b * c) (hle : c ≤ d) :

a < b * d

source

theorem lt_add_of_lt_add_right {α : Type u} [ordered_add_comm_monoid α] {a b c d : α} (h : a < b + c) (hle : b ≤ d) :

a < d + c

source

theorem lt_mul_of_lt_mul_right {α : Type u} [ordered_comm_monoid α] {a b c d : α} (h : a < b * c) (hle : b ≤ d) :

a < d * c

source

theorem le_add_of_le_add_left {α : Type u} [ordered_add_comm_monoid α] {a b c d : α} (h : a ≤ b + c) (hle : c ≤ d) :

a ≤ b + d

source

theorem le_mul_of_le_mul_left {α : Type u} [ordered_comm_monoid α] {a b c d : α} (h : a ≤ b * c) (hle : c ≤ d) :

a ≤ b * d

source

theorem le_mul_of_le_mul_right {α : Type u} [ordered_comm_monoid α] {a b c d : α} (h : a ≤ b * c) (hle : b ≤ d) :

a ≤ d * c

source

theorem le_add_of_le_add_right {α : Type u} [ordered_add_comm_monoid α] {a b c d : α} (h : a ≤ b + c) (hle : b ≤ d) :

a ≤ d + c

source

theorem lt_of_add_lt_add_left {α : Type u} [ordered_add_comm_monoid α] {a b c : α} :

a + b < a + c → b < c

source

theorem lt_of_mul_lt_mul_left' {α : Type u} [ordered_comm_monoid α] {a b c : α} :

a * b < a * c → b < c

source

theorem lt_of_add_lt_add_right {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (h : a + b < c + b) :

a < c

source

theorem lt_of_mul_lt_mul_right' {α : Type u} [ordered_comm_monoid α] {a b c : α} (h : a * b < c * b) :

a < c

source

theorem add_le_add {α : Type u} [ordered_add_comm_monoid α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) :

a + c ≤ b + d

source

theorem mul_le_mul' {α : Type u} [ordered_comm_monoid α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) :

a * c ≤ b * d

source

theorem mul_le_mul_three {α : Type u} [ordered_comm_monoid α] {a b c d e f : α} (h₁ : a ≤ d) (h₂ : b ≤ e) (h₃ : c ≤ f) :

(a * b) * c ≤ (d * e) * f

source

theorem add_le_add_three {α : Type u} [ordered_add_comm_monoid α] {a b c d e f : α} (h₁ : a ≤ d) (h₂ : b ≤ e) (h₃ : c ≤ f) :

a + b + c ≤ d + e + f

source

theorem le_add_of_nonneg_right {α : Type u} [ordered_add_comm_monoid α] {a b : α} (h : 0 ≤ b) :

a ≤ a + b

source

theorem le_mul_of_one_le_right' {α : Type u} [ordered_comm_monoid α] {a b : α} (h : 1 ≤ b) :

a ≤ a * b

source

theorem le_mul_of_one_le_left' {α : Type u} [ordered_comm_monoid α] {a b : α} (h : 1 ≤ b) :

a ≤ b * a

source

theorem le_add_of_nonneg_left {α : Type u} [ordered_add_comm_monoid α] {a b : α} (h : 0 ≤ b) :

a ≤ b + a

source

theorem mul_le_of_le_one_right' {α : Type u} [ordered_comm_monoid α] {a b : α} (h : b ≤ 1) :

a * b ≤ a

source

theorem add_le_of_nonpos_right {α : Type u} [ordered_add_comm_monoid α] {a b : α} (h : b ≤ 0) :

a + b ≤ a

source

theorem add_le_of_nonpos_left {α : Type u} [ordered_add_comm_monoid α] {a b : α} (h : b ≤ 0) :

b + a ≤ a

source

theorem mul_le_of_le_one_left' {α : Type u} [ordered_comm_monoid α] {a b : α} (h : b ≤ 1) :

b * a ≤ a

source

theorem lt_of_mul_lt_of_one_le_left {α : Type u} [ordered_comm_monoid α] {a b c : α} (h : a * b < c) (hle : 1 ≤ b) :

a < c

source

theorem lt_of_add_lt_of_nonneg_left {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (h : a + b < c) (hle : 0 ≤ b) :

a < c

source

theorem lt_of_mul_lt_of_one_le_right {α : Type u} [ordered_comm_monoid α] {a b c : α} (h : a * b < c) (hle : 1 ≤ a) :

b < c

source

theorem lt_of_add_lt_of_nonneg_right {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (h : a + b < c) (hle : 0 ≤ a) :

b < c

source

theorem le_of_mul_le_of_one_le_left {α : Type u} [ordered_comm_monoid α] {a b c : α} (h : a * b ≤ c) (hle : 1 ≤ b) :

a ≤ c

source

theorem le_of_add_le_of_nonneg_left {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (h : a + b ≤ c) (hle : 0 ≤ b) :

a ≤ c

source

theorem le_of_mul_le_of_one_le_right {α : Type u} [ordered_comm_monoid α] {a b c : α} (h : a * b ≤ c) (hle : 1 ≤ a) :

b ≤ c

source

theorem le_of_add_le_of_nonneg_right {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (h : a + b ≤ c) (hle : 0 ≤ a) :

b ≤ c

source

theorem lt_of_lt_add_of_nonpos_left {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (h : a < b + c) (hle : c ≤ 0) :

a < b

source

theorem lt_of_lt_mul_of_le_one_left {α : Type u} [ordered_comm_monoid α] {a b c : α} (h : a < b * c) (hle : c ≤ 1) :

a < b

source

theorem lt_of_lt_add_of_nonpos_right {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (h : a < b + c) (hle : b ≤ 0) :

a < c

source

theorem lt_of_lt_mul_of_le_one_right {α : Type u} [ordered_comm_monoid α] {a b c : α} (h : a < b * c) (hle : b ≤ 1) :

a < c

source

theorem le_of_le_add_of_nonpos_left {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (h : a ≤ b + c) (hle : c ≤ 0) :

a ≤ b

source

theorem le_of_le_mul_of_le_one_left {α : Type u} [ordered_comm_monoid α] {a b c : α} (h : a ≤ b * c) (hle : c ≤ 1) :

a ≤ b

source

theorem le_of_le_mul_of_le_one_right {α : Type u} [ordered_comm_monoid α] {a b c : α} (h : a ≤ b * c) (hle : b ≤ 1) :

a ≤ c

source

theorem le_of_le_add_of_nonpos_right {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (h : a ≤ b + c) (hle : b ≤ 0) :

a ≤ c

source

theorem le_add_of_nonneg_of_le {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (ha : 0 ≤ a) (hbc : b ≤ c) :

b ≤ a + c

source

theorem le_mul_of_one_le_of_le {α : Type u} [ordered_comm_monoid α] {a b c : α} (ha : 1 ≤ a) (hbc : b ≤ c) :

b ≤ a * c

source

theorem le_add_of_le_of_nonneg {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : 0 ≤ a) :

b ≤ c + a

source

theorem le_mul_of_le_of_one_le {α : Type u} [ordered_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : 1 ≤ a) :

b ≤ c * a

source

theorem one_le_mul {α : Type u} [ordered_comm_monoid α] {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) :

1 ≤ a * b

source

theorem add_nonneg {α : Type u} [ordered_add_comm_monoid α] {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) :

0 ≤ a + b

source

theorem one_lt_mul_of_lt_of_le' {α : Type u} [ordered_comm_monoid α] {a b : α} (ha : 1 < a) (hb : 1 ≤ b) :

1 < a * b

source

theorem add_pos_of_pos_of_nonneg {α : Type u} [ordered_add_comm_monoid α] {a b : α} (ha : 0 < a) (hb : 0 ≤ b) :

0 < a + b

source

theorem add_pos_of_nonneg_of_pos {α : Type u} [ordered_add_comm_monoid α] {a b : α} (ha : 0 ≤ a) (hb : 0 < b) :

0 < a + b

source

theorem one_lt_mul_of_le_of_lt' {α : Type u} [ordered_comm_monoid α] {a b : α} (ha : 1 ≤ a) (hb : 1 < b) :

1 < a * b

source

theorem one_lt_mul' {α : Type u} [ordered_comm_monoid α] {a b : α} (ha : 1 < a) (hb : 1 < b) :

1 < a * b

source

theorem add_pos {α : Type u} [ordered_add_comm_monoid α] {a b : α} (ha : 0 < a) (hb : 0 < b) :

0 < a + b

source

theorem add_nonpos {α : Type u} [ordered_add_comm_monoid α] {a b : α} (ha : a ≤ 0) (hb : b ≤ 0) :

a + b ≤ 0

source

theorem mul_le_one' {α : Type u} [ordered_comm_monoid α] {a b : α} (ha : a ≤ 1) (hb : b ≤ 1) :

a * b ≤ 1

source

theorem mul_le_of_le_one_of_le' {α : Type u} [ordered_comm_monoid α] {a b c : α} (ha : a ≤ 1) (hbc : b ≤ c) :

a * b ≤ c

source

theorem add_le_of_nonpos_of_le' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (ha : a ≤ 0) (hbc : b ≤ c) :

a + b ≤ c

source

theorem add_le_of_le_of_nonpos' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : a ≤ 0) :

b + a ≤ c

source

theorem mul_le_of_le_of_le_one' {α : Type u} [ordered_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : a ≤ 1) :

b * a ≤ c

source

theorem add_neg_of_neg_of_nonpos' {α : Type u} [ordered_add_comm_monoid α] {a b : α} (ha : a < 0) (hb : b ≤ 0) :

a + b < 0

source

theorem mul_lt_one_of_lt_one_of_le_one' {α : Type u} [ordered_comm_monoid α] {a b : α} (ha : a < 1) (hb : b ≤ 1) :

a * b < 1

source

theorem mul_lt_one_of_le_one_of_lt_one' {α : Type u} [ordered_comm_monoid α] {a b : α} (ha : a ≤ 1) (hb : b < 1) :

a * b < 1

source

theorem add_neg_of_nonpos_of_neg' {α : Type u} [ordered_add_comm_monoid α] {a b : α} (ha : a ≤ 0) (hb : b < 0) :

a + b < 0

source

theorem mul_lt_one' {α : Type u} [ordered_comm_monoid α] {a b : α} (ha : a < 1) (hb : b < 1) :

a * b < 1

source

theorem add_neg' {α : Type u} [ordered_add_comm_monoid α] {a b : α} (ha : a < 0) (hb : b < 0) :

a + b < 0

source

theorem lt_mul_of_one_le_of_lt' {α : Type u} [ordered_comm_monoid α] {a b c : α} (ha : 1 ≤ a) (hbc : b < c) :

b < a * c

source

theorem lt_add_of_nonneg_of_lt' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (ha : 0 ≤ a) (hbc : b < c) :

b < a + c

source

theorem lt_mul_of_lt_of_one_le' {α : Type u} [ordered_comm_monoid α] {a b c : α} (hbc : b < c) (ha : 1 ≤ a) :

b < c * a

source

theorem lt_add_of_lt_of_nonneg' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (hbc : b < c) (ha : 0 ≤ a) :

b < c + a

source

theorem lt_add_of_pos_of_lt' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (ha : 0 < a) (hbc : b < c) :

b < a + c

source

theorem lt_mul_of_one_lt_of_lt' {α : Type u} [ordered_comm_monoid α] {a b c : α} (ha : 1 < a) (hbc : b < c) :

b < a * c

source

theorem lt_add_of_lt_of_pos' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (hbc : b < c) (ha : 0 < a) :

b < c + a

source

theorem lt_mul_of_lt_of_one_lt' {α : Type u} [ordered_comm_monoid α] {a b c : α} (hbc : b < c) (ha : 1 < a) :

b < c * a

source

theorem add_lt_of_nonpos_of_lt' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (ha : a ≤ 0) (hbc : b < c) :

a + b < c

source

theorem mul_lt_of_le_one_of_lt' {α : Type u} [ordered_comm_monoid α] {a b c : α} (ha : a ≤ 1) (hbc : b < c) :

a * b < c

source

theorem mul_lt_of_lt_of_le_one' {α : Type u} [ordered_comm_monoid α] {a b c : α} (hbc : b < c) (ha : a ≤ 1) :

b * a < c

source

theorem add_lt_of_lt_of_nonpos' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (hbc : b < c) (ha : a ≤ 0) :

b + a < c

source

theorem mul_lt_of_lt_one_of_lt' {α : Type u} [ordered_comm_monoid α] {a b c : α} (ha : a < 1) (hbc : b < c) :

a * b < c

source

theorem add_lt_of_neg_of_lt' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (ha : a < 0) (hbc : b < c) :

a + b < c

source

theorem mul_lt_of_lt_of_lt_one' {α : Type u} [ordered_comm_monoid α] {a b c : α} (hbc : b < c) (ha : a < 1) :

b * a < c

source

theorem add_lt_of_lt_of_neg' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (hbc : b < c) (ha : a < 0) :

b + a < c

source

theorem add_eq_zero_iff' {α : Type u} [ordered_add_comm_monoid α] {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) :

a + b = 0 ↔ a = 0 ∧ b = 0

source

theorem mul_eq_one_iff' {α : Type u} [ordered_comm_monoid α] {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) :

a * b = 1 ↔ a = 1 ∧ b = 1

source

def function.injective.ordered_comm_monoid {α : Type u} [ordered_comm_monoid α] {β : Type u_1} [has_one β] [has_mul β] (f : β → α) (hf : function.injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) :

ordered_comm_monoid β

Pullback an ordered_comm_monoid under an injective map.

Equations

function.injective.ordered_comm_monoid f hf one mul = {mul := comm_monoid.mul (function.injective.comm_monoid f hf one mul), mul_assoc := _, one := comm_monoid.one (function.injective.comm_monoid f hf one mul), one_mul := _, mul_one := _, mul_comm := _, le := partial_order.le (partial_order.lift f hf), lt := partial_order.lt (partial_order.lift f hf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, lt_of_mul_lt_mul_left := _}

source

def function.injective.ordered_add_comm_monoid {α : Type u} [ordered_add_comm_monoid α] {β : Type u_1} [has_zero β] [has_add β] (f : β → α) (hf : function.injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) :

ordered_add_comm_monoid β

Pullback an ordered_add_comm_monoid under an injective map.

source

theorem monotone.mul' {α : Type u} [ordered_comm_monoid α] {β : Type u_1} [preorder β] {f g : β → α} (hf : monotone f) (hg : monotone g) :

monotone (λ (x : β), (f x) * g x)

source

theorem monotone.add {α : Type u} [ordered_add_comm_monoid α] {β : Type u_1} [preorder β] {f g : β → α} (hf : monotone f) (hg : monotone g) :

monotone (λ (x : β), f x + g x)

source

theorem monotone.add_const {α : Type u} [ordered_add_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : monotone f) (a : α) :

monotone (λ (x : β), f x + a)

source

theorem monotone.mul_const' {α : Type u} [ordered_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : monotone f) (a : α) :

monotone (λ (x : β), (f x) * a)

source

theorem monotone.const_add {α : Type u} [ordered_add_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : monotone f) (a : α) :

monotone (λ (x : β), a + f x)

source

theorem monotone.const_mul' {α : Type u} [ordered_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : monotone f) (a : α) :

monotone (λ (x : β), a * f x)

source

def function.injective.linear_ordered_comm_monoid {α : Type u} [linear_ordered_comm_monoid α] {β : Type u_1} [has_one β] [has_mul β] (f : β → α) (hf : function.injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) :

linear_ordered_comm_monoid β

Pullback a linear_ordered_comm_monoid under an injective map.

Equations

function.injective.linear_ordered_comm_monoid f hf one mul = {le := ordered_comm_monoid.le (function.injective.ordered_comm_monoid f hf one mul), lt := ordered_comm_monoid.lt (function.injective.ordered_comm_monoid f hf one mul), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le (linear_order.lift f hf), decidable_eq := linear_order.decidable_eq (linear_order.lift f hf), decidable_lt := linear_order.decidable_lt (linear_order.lift f hf), mul := ordered_comm_monoid.mul (function.injective.ordered_comm_monoid f hf one mul), mul_assoc := _, one := ordered_comm_monoid.one (function.injective.ordered_comm_monoid f hf one mul), one_mul := _, mul_one := _, mul_comm := _, mul_le_mul_left := _, lt_of_mul_lt_mul_left := _}

source

def function.injective.linear_ordered_add_comm_monoid {α : Type u} [linear_ordered_add_comm_monoid α] {β : Type u_1} [has_zero β] [has_add β] (f : β → α) (hf : function.injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) :

linear_ordered_add_comm_monoid β

Pullback an ordered_add_comm_monoid under an injective map.

source

theorem bit0_pos {α : Type u} [ordered_add_comm_monoid α] {a : α} (h : 0 < a) :

0 < bit0 a

source

@[instance]

def add_units.preorder {α : Type u} [add_monoid α] [preorder α] :

preorder (add_units α)

source

@[instance]

def units.preorder {α : Type u} [monoid α] [preorder α] :

preorder (units α)

Equations

units.preorder = preorder.lift coe

source

@[simp]

theorem add_units.coe_le_coe {α : Type u} [add_monoid α] [preorder α] {a b : add_units α} :

↑a ≤ ↑b ↔ a ≤ b

source

@[simp]

theorem units.coe_le_coe {α : Type u} [monoid α] [preorder α] {a b : units α} :

↑a ≤ ↑b ↔ a ≤ b

source

@[simp]

theorem add_units.coe_lt_coe {α : Type u} [add_monoid α] [preorder α] {a b : add_units α} :

↑a < ↑b ↔ a < b

source

@[simp]

theorem units.coe_lt_coe {α : Type u} [monoid α] [preorder α] {a b : units α} :

↑a < ↑b ↔ a < b

source

@[instance]

def add_units.partial_order {α : Type u} [add_monoid α] [partial_order α] :

partial_order (add_units α)

source

@[instance]

def units.partial_order {α : Type u} [monoid α] [partial_order α] :

partial_order (units α)

Equations

units.partial_order = partial_order.lift coe units.ext

source

@[instance]

def units.linear_order {α : Type u} [monoid α] [linear_order α] :

linear_order (units α)

Equations

units.linear_order = linear_order.lift coe units.ext

source

@[instance]

def add_units.linear_order {α : Type u} [add_monoid α] [linear_order α] :

linear_order (add_units α)

source

@[simp]

theorem add_units.max_coe {α : Type u} [add_monoid α] [linear_order α] {a b : add_units α} :

↑(max a b) = max ↑a ↑b

source

@[simp]

theorem units.max_coe {α : Type u} [monoid α] [linear_order α] {a b : units α} :

↑(max a b) = max ↑a ↑b

source

@[simp]

theorem units.min_coe {α : Type u} [monoid α] [linear_order α] {a b : units α} :

↑(min a b) = min ↑a ↑b

source

@[simp]

theorem add_units.min_coe {α : Type u} [add_monoid α] [linear_order α] {a b : add_units α} :

↑(min a b) = min ↑a ↑b

source

@[instance]

def with_zero.preorder {α : Type u} [preorder α] :

preorder (with_zero α)

Equations

with_zero.preorder = with_bot.preorder

source

@[instance]

def with_zero.partial_order {α : Type u} [partial_order α] :

partial_order (with_zero α)

Equations

with_zero.partial_order = with_bot.partial_order

source

@[instance]

def with_zero.order_bot {α : Type u} [partial_order α] :

order_bot (with_zero α)

Equations

with_zero.order_bot = with_bot.order_bot

source

theorem with_zero.zero_le {α : Type u} [partial_order α] (a : with_zero α) :

0 ≤ a

source

theorem with_zero.zero_lt_coe {α : Type u} [partial_order α] (a : α) :

0 < ↑a

source

@[simp]

theorem with_zero.coe_lt_coe {α : Type u} [partial_order α] {a b : α} :

↑a < ↑b ↔ a < b

source

@[simp]

theorem with_zero.coe_le_coe {α : Type u} [partial_order α] {a b : α} :

↑a ≤ ↑b ↔ a ≤ b

source

@[instance]

def with_zero.lattice {α : Type u} [lattice α] :

lattice (with_zero α)

Equations

with_zero.lattice = with_bot.lattice

source

@[instance]

def with_zero.linear_order {α : Type u} [linear_order α] :

linear_order (with_zero α)

Equations

with_zero.linear_order = with_bot.linear_order

source

theorem with_zero.mul_le_mul_left {α : Type u} [ordered_comm_monoid α] (a b : with_zero α) :

a ≤ b → ∀ (c : with_zero α), c * a ≤ c * b

source

theorem with_zero.lt_of_mul_lt_mul_left {α : Type u} [ordered_comm_monoid α] (a b c : with_zero α) :

a * b < a * c → b < c

source

@[instance]

def with_zero.ordered_comm_monoid {α : Type u} [ordered_comm_monoid α] :

ordered_comm_monoid (with_zero α)

Equations

with_zero.ordered_comm_monoid = {mul := comm_monoid_with_zero.mul with_zero.comm_monoid_with_zero, mul_assoc := _, one := comm_monoid_with_zero.one with_zero.comm_monoid_with_zero, one_mul := _, mul_one := _, mul_comm := _, le := partial_order.le with_zero.partial_order, lt := partial_order.lt with_zero.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, lt_of_mul_lt_mul_left := _}

source

def with_zero.ordered_add_comm_monoid {α : Type u} [ordered_add_comm_monoid α] (zero_le : ∀ (a : α), 0 ≤ a) :

ordered_add_comm_monoid (with_zero α)

If 0 is the least element in α, then with_zero α is an ordered_add_comm_monoid.

Equations

with_zero.ordered_add_comm_monoid zero_le = {add := add_comm_monoid.add with_zero.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero with_zero.add_comm_monoid, zero_add := _, add_zero := _, add_comm := _, le := partial_order.le with_zero.partial_order, lt := partial_order.lt with_zero.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _}

source

@[instance]

def with_top.has_one {α : Type u} [has_one α] :

has_one (with_top α)

Equations

with_top.has_one = {one := ↑1}

source

@[instance]

def with_top.has_zero {α : Type u} [has_zero α] :

has_zero (with_top α)

source

@[simp]

theorem with_top.coe_one {α : Type u} [has_one α] :

↑1 = 1

source

@[simp]

theorem with_top.coe_zero {α : Type u} [has_zero α] :

↑0 = 0

source

@[simp]

theorem with_top.coe_eq_zero {α : Type u} [has_zero α] {a : α} :

↑a = 0 ↔ a = 0

source

@[simp]

theorem with_top.coe_eq_one {α : Type u} [has_one α] {a : α} :

↑a = 1 ↔ a = 1

source

@[simp]

theorem with_top.zero_eq_coe {α : Type u} [has_zero α] {a : α} :

0 = ↑a ↔ a = 0

source

@[simp]

theorem with_top.one_eq_coe {α : Type u} [has_one α] {a : α} :

1 = ↑a ↔ a = 1

source

@[simp]

theorem with_top.top_ne_one {α : Type u} [has_one α] :

⊤ ≠ 1

source

@[simp]

theorem with_top.top_ne_zero {α : Type u} [has_zero α] :

⊤ ≠ 0

source

@[simp]

theorem with_top.zero_ne_top {α : Type u} [has_zero α] :

0 ≠ ⊤

source

@[simp]

theorem with_top.one_ne_top {α : Type u} [has_one α] :

1 ≠ ⊤

source

@[instance]

def with_top.has_add {α : Type u} [has_add α] :

has_add (with_top α)

Equations

with_top.has_add = {add := λ (o₁ o₂ : with_top α), option.bind o₁ (λ (a : α), option.map (λ (b : α), a + b) o₂)}

source

@[instance]

def with_top.add_semigroup {α : Type u} [add_semigroup α] :

add_semigroup (with_top α)

Equations

with_top.add_semigroup = {add := has_add.add with_top.has_add, add_assoc := _}

source

theorem with_top.coe_add {α : Type u} [has_add α] {a b : α} :

↑(a + b) = ↑a + ↑b

source

theorem with_top.coe_bit0 {α : Type u} [has_add α] {a : α} :

↑(bit0 a) = bit0 ↑a

source

theorem with_top.coe_bit1 {α : Type u} [has_add α] [has_one α] {a : α} :

↑(bit1 a) = bit1 ↑a

source

@[simp]

theorem with_top.add_top {α : Type u} [has_add α] {a : with_top α} :

a + ⊤ = ⊤

source

@[simp]

theorem with_top.top_add {α : Type u} [has_add α] {a : with_top α} :

⊤ + a = ⊤

source

theorem with_top.add_eq_top {α : Type u} [has_add α] {a b : with_top α} :

a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤

source

theorem with_top.add_lt_top {α : Type u} [has_add α] [partial_order α] {a b : with_top α} :

a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤

source

theorem with_top.add_eq_coe {α : Type u} [has_add α] {a b : with_top α} {c : α} :

a + b = ↑c ↔ ∃ (a' b' : α), ↑a' = a ∧ ↑b' = b ∧ a' + b' = c

source

@[instance]

def with_top.add_comm_semigroup {α : Type u} [add_comm_semigroup α] :

add_comm_semigroup (with_top α)

Equations

with_top.add_comm_semigroup = {add := add_comm_semigroup.add additive.add_comm_semigroup, add_assoc := _, add_comm := _}

source

@[instance]

def with_top.add_monoid {α : Type u} [add_monoid α] :

add_monoid (with_top α)

Equations

with_top.add_monoid = {add := has_add.add with_top.has_add, add_assoc := _, zero := some 0, zero_add := _, add_zero := _}

source

@[instance]

def with_top.add_comm_monoid {α : Type u} [add_comm_monoid α] :

add_comm_monoid (with_top α)

Equations

with_top.add_comm_monoid = {add := has_add.add with_top.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, add_comm := _}

source

@[instance]

def with_top.ordered_add_comm_monoid {α : Type u} [ordered_add_comm_monoid α] :

ordered_add_comm_monoid (with_top α)

Equations

with_top.ordered_add_comm_monoid = {add := add_comm_monoid.add with_top.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero with_top.add_comm_monoid, zero_add := _, add_zero := _, add_comm := _, le := partial_order.le with_top.partial_order, lt := partial_order.lt with_top.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _}

source

@[instance]

def with_top.linear_ordered_add_comm_monoid_with_top {α : Type u} [linear_ordered_add_comm_monoid α] :

linear_ordered_add_comm_monoid_with_top (with_top α)

Equations

with_top.linear_ordered_add_comm_monoid_with_top = {le := order_top.le with_top.order_top, lt := order_top.lt with_top.order_top, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le with_top.linear_order, decidable_eq := linear_order.decidable_eq with_top.linear_order, decidable_lt := linear_order.decidable_lt with_top.linear_order, add := ordered_add_comm_monoid.add with_top.ordered_add_comm_monoid, add_assoc := _, zero := ordered_add_comm_monoid.zero with_top.ordered_add_comm_monoid, zero_add := _, add_zero := _, add_comm := _, add_le_add_left := _, lt_of_add_lt_add_left := _, top := order_top.top with_top.order_top, le_top := _, top_add' := _}

source

def with_top.coe_add_hom {α : Type u} [add_monoid α] :

α →+ with_top α

Coercion from α to with_top α as an add_monoid_hom.

Equations

with_top.coe_add_hom = {to_fun := coe coe_to_lift, map_zero' := _, map_add' := _}

source

@[simp]

theorem with_top.coe_coe_add_hom {α : Type u} [add_monoid α] :

⇑with_top.coe_add_hom = coe

source

@[simp]

theorem with_top.zero_lt_top {α : Type u} [ordered_add_comm_monoid α] :

0 < ⊤

source

@[simp]

theorem with_top.zero_lt_coe {α : Type u} [ordered_add_comm_monoid α] (a : α) :

0 < ↑a ↔ 0 < a

source

@[instance]

def with_bot.has_zero {α : Type u} [has_zero α] :

has_zero (with_bot α)

Equations

with_bot.has_zero = with_top.has_zero

source

@[instance]

def with_bot.has_one {α : Type u} [has_one α] :

has_one (with_bot α)

Equations

with_bot.has_one = with_top.has_one

source

@[instance]

def with_bot.add_semigroup {α : Type u} [add_semigroup α] :

add_semigroup (with_bot α)

Equations

with_bot.add_semigroup = with_top.add_semigroup

source

@[instance]

def with_bot.add_comm_semigroup {α : Type u} [add_comm_semigroup α] :

add_comm_semigroup (with_bot α)

Equations

with_bot.add_comm_semigroup = with_top.add_comm_semigroup

source

@[instance]

def with_bot.add_monoid {α : Type u} [add_monoid α] :

add_monoid (with_bot α)

Equations

with_bot.add_monoid = with_top.add_monoid

source

@[instance]

def with_bot.add_comm_monoid {α : Type u} [add_comm_monoid α] :

add_comm_monoid (with_bot α)

Equations

with_bot.add_comm_monoid = with_top.add_comm_monoid

source

@[instance]

def with_bot.ordered_add_comm_monoid {α : Type u} [ordered_add_comm_monoid α] :

ordered_add_comm_monoid (with_bot α)

Equations

with_bot.ordered_add_comm_monoid = {add := add_comm_monoid.add with_bot.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero with_bot.add_comm_monoid, zero_add := _, add_zero := _, add_comm := _, le := partial_order.le with_bot.partial_order, lt := partial_order.lt with_bot.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _}

source

theorem with_bot.coe_zero {α : Type u} [has_zero α] :

↑0 = 0

source

theorem with_bot.coe_one {α : Type u} [has_one α] :

↑1 = 1

source

theorem with_bot.coe_eq_zero {α : Type u_1} [add_monoid α] {a : α} :

↑a = 0 ↔ a = 0

source

theorem with_bot.coe_add {α : Type u} [add_semigroup α] (a b : α) :

↑(a + b) = ↑a + ↑b

source

theorem with_bot.coe_bit0 {α : Type u} [add_semigroup α] {a : α} :

↑(bit0 a) = bit0 ↑a

source

theorem with_bot.coe_bit1 {α : Type u} [add_semigroup α] [has_one α] {a : α} :

↑(bit1 a) = bit1 ↑a

source

@[simp]

theorem with_bot.bot_add {α : Type u} [ordered_add_comm_monoid α] (a : with_bot α) :

⊥ + a = ⊥

source

@[simp]

theorem with_bot.add_bot {α : Type u} [ordered_add_comm_monoid α] (a : with_bot α) :

a + ⊥ = ⊥

source

@[instance]

def canonically_ordered_add_monoid.to_ordered_add_comm_monoid (α : Type u_1) [s : canonically_ordered_add_monoid α] :

ordered_add_comm_monoid α

source

@[instance]

def canonically_ordered_add_monoid.to_order_bot (α : Type u_1) [s : canonically_ordered_add_monoid α] :

order_bot α

source

@[class]

structure canonically_ordered_add_monoid (α : Type u_1) :

Type u_1

add : α → α → α
add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
add_comm : ∀ (a b : α), a + b = b + a
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b
lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1 → b < c_1
bot : α
bot_le : ∀ (a : α), ⊥ ≤ a
le_iff_exists_add : ∀ (a b : α), a ≤ b ↔ ∃ (c_1 : α), b = a + c_1

A canonically ordered additive monoid is an ordered commutative additive monoid in which the ordering coincides with the subtractibility relation, which is to say, a ≤ b iff there exists c with b = a + c. This is satisfied by the natural numbers, for example, but not the integers or other nontrivial ordered_add_comm_groups.

Instances

source

@[instance]

def canonically_ordered_monoid.to_order_bot (α : Type u_1) [s : canonically_ordered_monoid α] :

order_bot α

source

@[instance]

def canonically_ordered_monoid.to_ordered_comm_monoid (α : Type u_1) [s : canonically_ordered_monoid α] :

ordered_comm_monoid α

source

@[class]

structure canonically_ordered_monoid (α : Type u_1) :

Type u_1

mul : α → α → α
mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
mul_comm : ∀ (a b : α), a * b = b * a
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 * a ≤ c_1 * b
lt_of_mul_lt_mul_left : ∀ (a b c_1 : α), a * b < a * c_1 → b < c_1
bot : α
bot_le : ∀ (a : α), ⊥ ≤ a
le_iff_exists_mul : ∀ (a b : α), a ≤ b ↔ ∃ (c_1 : α), b = a * c_1

A canonically ordered monoid is an ordered commutative monoid in which the ordering coincides with the divisibility relation, which is to say, a ≤ b iff there exists c with b = a * c. Example seem rare; it seems more likely that the order_dual of a naturally-occurring lattice satisfies this than the lattice itself (for example, dual of the lattice of ideals of a PID or Dedekind domain satisfy this; collections of all things ≤ 1 seem to be more natural that collections of all things ≥ 1).

Instances

canonically_linear_ordered_monoid.to_canonically_ordered_monoid

source

theorem le_iff_exists_add {α : Type u} [canonically_ordered_add_monoid α] {a b : α} :

a ≤ b ↔ ∃ (c : α), b = a + c

source

theorem le_iff_exists_mul {α : Type u} [canonically_ordered_monoid α] {a b : α} :

a ≤ b ↔ ∃ (c : α), b = a * c

source

theorem self_le_mul_right {α : Type u} [canonically_ordered_monoid α] (a b : α) :

a ≤ a * b

source

theorem self_le_add_right {α : Type u} [canonically_ordered_add_monoid α] (a b : α) :

a ≤ a + b

source

theorem self_le_add_left {α : Type u} [canonically_ordered_add_monoid α] (a b : α) :

a ≤ b + a

source

theorem self_le_mul_left {α : Type u} [canonically_ordered_monoid α] (a b : α) :

a ≤ b * a

source

@[simp]

theorem one_le {α : Type u} [canonically_ordered_monoid α] (a : α) :

1 ≤ a

source

@[simp]

theorem zero_le {α : Type u} [canonically_ordered_add_monoid α] (a : α) :

0 ≤ a

source

@[simp]

theorem bot_eq_one {α : Type u} [canonically_ordered_monoid α] :

⊥ = 1

source

@[simp]

theorem bot_eq_zero {α : Type u} [canonically_ordered_add_monoid α] :

⊥ = 0

source

@[simp]

theorem mul_eq_one_iff {α : Type u} [canonically_ordered_monoid α] {a b : α} :

a * b = 1 ↔ a = 1 ∧ b = 1

source

@[simp]

theorem add_eq_zero_iff {α : Type u} [canonically_ordered_add_monoid α] {a b : α} :

a + b = 0 ↔ a = 0 ∧ b = 0

source

@[simp]

theorem le_one_iff_eq_one {α : Type u} [canonically_ordered_monoid α] {a : α} :

a ≤ 1 ↔ a = 1

source

@[simp]

theorem nonpos_iff_eq_zero {α : Type u} [canonically_ordered_add_monoid α] {a : α} :

a ≤ 0 ↔ a = 0

source

theorem one_lt_iff_ne_one {α : Type u} [canonically_ordered_monoid α] {a : α} :

1 < a ↔ a ≠ 1

source

theorem pos_iff_ne_zero {α : Type u} [canonically_ordered_add_monoid α] {a : α} :

0 < a ↔ a ≠ 0

source

theorem exists_pos_mul_of_lt {α : Type u} [canonically_ordered_monoid α] {a b : α} (h : a < b) :

∃ (c : α) (H : c > 1), a * c = b

source

theorem exists_pos_add_of_lt {α : Type u} [canonically_ordered_add_monoid α] {a b : α} (h : a < b) :

∃ (c : α) (H : c > 0), a + c = b

source

theorem le_add_left {α : Type u} [canonically_ordered_add_monoid α] {a b c : α} (h : a ≤ c) :

a ≤ b + c

source

theorem le_mul_left {α : Type u} [canonically_ordered_monoid α] {a b c : α} (h : a ≤ c) :

a ≤ b * c

source

theorem le_add_right {α : Type u} [canonically_ordered_add_monoid α] {a b c : α} (h : a ≤ b) :

a ≤ b + c

source

theorem le_mul_right {α : Type u} [canonically_ordered_monoid α] {a b c : α} (h : a ≤ b) :

a ≤ b * c

source

@[instance]

def with_zero.canonically_ordered_add_monoid {α : Type u} [canonically_ordered_add_monoid α] :

canonically_ordered_add_monoid (with_zero α)

Adding a new zero to a canonically ordered additive monoid produces another one.

Equations

with_zero.canonically_ordered_add_monoid = {add := ordered_add_comm_monoid.add (with_zero.ordered_add_comm_monoid zero_le), add_assoc := _, zero := ordered_add_comm_monoid.zero (with_zero.ordered_add_comm_monoid zero_le), zero_add := _, add_zero := _, add_comm := _, le := ordered_add_comm_monoid.le (with_zero.ordered_add_comm_monoid zero_le), lt := ordered_add_comm_monoid.lt (with_zero.ordered_add_comm_monoid zero_le), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _, bot := 0, bot_le := _, le_iff_exists_add := _}

source

@[instance]

def with_top.canonically_ordered_add_monoid {α : Type u} [canonically_ordered_add_monoid α] :

canonically_ordered_add_monoid (with_top α)

Equations

with_top.canonically_ordered_add_monoid = {add := ordered_add_comm_monoid.add with_top.ordered_add_comm_monoid, add_assoc := _, zero := ordered_add_comm_monoid.zero with_top.ordered_add_comm_monoid, zero_add := _, add_zero := _, add_comm := _, le := order_bot.le with_top.order_bot, lt := order_bot.lt with_top.order_bot, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _, bot := order_bot.bot with_top.order_bot, bot_le := _, le_iff_exists_add := _}

source

@[instance]

def canonically_ordered_monoid.has_exists_mul_of_le (α : Type u) [canonically_ordered_monoid α] :

has_exists_mul_of_le α

source

@[instance]

def canonically_ordered_add_monoid.has_exists_add_of_le (α : Type u) [canonically_ordered_add_monoid α] :

has_exists_add_of_le α

source

@[instance]

def canonically_linear_ordered_add_monoid.to_linear_order (α : Type u_1) [s : canonically_linear_ordered_add_monoid α] :

linear_order α

source

@[instance]

def canonically_linear_ordered_add_monoid.to_canonically_ordered_add_monoid (α : Type u_1) [s : canonically_linear_ordered_add_monoid α] :

canonically_ordered_add_monoid α

source

@[class]

structure canonically_linear_ordered_add_monoid (α : Type u_1) :

Type u_1

add : α → α → α
add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
add_comm : ∀ (a b : α), a + b = b + a
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b
lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1 → b < c_1
bot : α
bot_le : ∀ (a : α), ⊥ ≤ a
le_iff_exists_add : ∀ (a b : α), a ≤ b ↔ ∃ (c_1 : α), b = a + c_1
le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
decidable_le : decidable_rel has_le.le
decidable_eq : decidable_eq α
decidable_lt : decidable_rel has_lt.lt

A canonically linear-ordered additive monoid is a canonically ordered additive monoid whose ordering is a linear order.

Instances

source

@[instance]

def canonically_linear_ordered_monoid.to_linear_order (α : Type u_1) [s : canonically_linear_ordered_monoid α] :

linear_order α

source

@[instance]

def canonically_linear_ordered_monoid.to_canonically_ordered_monoid (α : Type u_1) [s : canonically_linear_ordered_monoid α] :

canonically_ordered_monoid α

source

@[class]

structure canonically_linear_ordered_monoid (α : Type u_1) :

Type u_1

mul : α → α → α
mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
mul_comm : ∀ (a b : α), a * b = b * a
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 * a ≤ c_1 * b
lt_of_mul_lt_mul_left : ∀ (a b c_1 : α), a * b < a * c_1 → b < c_1
bot : α
bot_le : ∀ (a : α), ⊥ ≤ a
le_iff_exists_mul : ∀ (a b : α), a ≤ b ↔ ∃ (c_1 : α), b = a * c_1
le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
decidable_le : decidable_rel has_le.le
decidable_eq : decidable_eq α
decidable_lt : decidable_rel has_lt.lt

A canonically linear-ordered monoid is a canonically ordered monoid whose ordering is a linear order.

source

@[instance]

def canonically_linear_ordered_add_monoid.semilattice_sup_bot {α : Type u} [canonically_linear_ordered_add_monoid α] :

semilattice_sup_bot α

source

@[instance]

def canonically_linear_ordered_monoid.semilattice_sup_bot {α : Type u} [canonically_linear_ordered_monoid α] :

semilattice_sup_bot α

Equations

canonically_linear_ordered_monoid.semilattice_sup_bot = {bot := order_bot.bot (canonically_ordered_monoid.to_order_bot α), le := lattice.le lattice_of_linear_order, lt := lattice.lt lattice_of_linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, sup := lattice.sup lattice_of_linear_order, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[instance]

def with_top.canonically_linear_ordered_add_monoid (α : Type u_1) [canonically_linear_ordered_add_monoid α] :

canonically_linear_ordered_add_monoid (with_top α)

Equations

with_top.canonically_linear_ordered_add_monoid α = {add := canonically_ordered_add_monoid.add infer_instance, add_assoc := _, zero := canonically_ordered_add_monoid.zero infer_instance, zero_add := _, add_zero := _, add_comm := _, le := canonically_ordered_add_monoid.le infer_instance, lt := canonically_ordered_add_monoid.lt infer_instance, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _, bot := canonically_ordered_add_monoid.bot infer_instance, bot_le := _, le_iff_exists_add := _, le_total := _, decidable_le := linear_order.decidable_le infer_instance, decidable_eq := linear_order.decidable_eq infer_instance, decidable_lt := linear_order.decidable_lt infer_instance}

source

theorem min_add_distrib {α : Type u} [canonically_linear_ordered_add_monoid α] (a b c : α) :

min a (b + c) = min a (min a b + min a c)

source

theorem min_mul_distrib {α : Type u} [canonically_linear_ordered_monoid α] (a b c : α) :

min a (b * c) = min a ((min a b) * min a c)

source

theorem min_mul_distrib' {α : Type u} [canonically_linear_ordered_monoid α] (a b c : α) :

min (a * b) c = min ((min a c) * min b c) c

source

theorem min_add_distrib' {α : Type u} [canonically_linear_ordered_add_monoid α] (a b c : α) :

min (a + b) c = min (min a c + min b c) c

source

@[class]

structure ordered_cancel_add_comm_monoid (α : Type u) :

Type u

add : α → α → α
add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
add_left_cancel : ∀ (a b c_1 : α), a + b = a + c_1 → b = c_1
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
add_comm : ∀ (a b : α), a + b = b + a
add_right_cancel : ∀ (a b c_1 : α), a + b = c_1 + b → a = c_1
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b
le_of_add_le_add_left : ∀ (a b c_1 : α), a + b ≤ a + c_1 → b ≤ c_1

An ordered cancellative additive commutative monoid is an additive commutative monoid with a partial order, in which addition is cancellative and monotone.

Instances

source

@[instance]

def ordered_cancel_add_comm_monoid.to_add_cancel_comm_monoid (α : Type u) [s : ordered_cancel_add_comm_monoid α] :

add_cancel_comm_monoid α

source

@[instance]

def ordered_cancel_add_comm_monoid.to_partial_order (α : Type u) [s : ordered_cancel_add_comm_monoid α] :

partial_order α

source

@[instance]

def ordered_cancel_comm_monoid.to_partial_order (α : Type u) [s : ordered_cancel_comm_monoid α] :

partial_order α

source

@[instance]

def ordered_cancel_comm_monoid.to_cancel_comm_monoid (α : Type u) [s : ordered_cancel_comm_monoid α] :

cancel_comm_monoid α

source

@[class]

structure ordered_cancel_comm_monoid (α : Type u) :

Type u

mul : α → α → α
mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
mul_left_cancel : ∀ (a b c_1 : α), a * b = a * c_1 → b = c_1
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
mul_comm : ∀ (a b : α), a * b = b * a
mul_right_cancel : ∀ (a b c_1 : α), a * b = c_1 * b → a = c_1
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 * a ≤ c_1 * b
le_of_mul_le_mul_left : ∀ (a b c_1 : α), a * b ≤ a * c_1 → b ≤ c_1

An ordered cancellative commutative monoid is a commutative monoid with a partial order, in which multiplication is cancellative and monotone.

Instances

source

theorem le_of_mul_le_mul_left' {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :

a * b ≤ a * c → b ≤ c

source

theorem le_of_add_le_add_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :

a + b ≤ a + c → b ≤ c

source

@[instance]

def ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid {α : Type u} [ordered_cancel_add_comm_monoid α] :

ordered_add_comm_monoid α

source

@[instance]

def ordered_cancel_comm_monoid.to_ordered_comm_monoid {α : Type u} [ordered_cancel_comm_monoid α] :

ordered_comm_monoid α

Equations

ordered_cancel_comm_monoid.to_ordered_comm_monoid = {mul := ordered_cancel_comm_monoid.mul _inst_1, mul_assoc := _, one := ordered_cancel_comm_monoid.one _inst_1, one_mul := _, mul_one := _, mul_comm := _, le := ordered_cancel_comm_monoid.le _inst_1, lt := ordered_cancel_comm_monoid.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, lt_of_mul_lt_mul_left := _}

source

theorem add_lt_add_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (h : a < b) (c : α) :

c + a < c + b

source

theorem mul_lt_mul_left' {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (h : a < b) (c : α) :

c * a < c * b

source

theorem mul_lt_mul_right' {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (h : a < b) (c : α) :

a * c < b * c

source

theorem add_lt_add_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (h : a < b) (c : α) :

a + c < b + c

source

theorem mul_lt_mul''' {α : Type u} [ordered_cancel_comm_monoid α] {a b c d : α} (h₁ : a < b) (h₂ : c < d) :

a * c < b * d

source

theorem add_lt_add {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c d : α} (h₁ : a < b) (h₂ : c < d) :

a + c < b + d

source

theorem mul_lt_mul_of_le_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c < d) :

a * c < b * d

source

theorem add_lt_add_of_le_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c < d) :

a + c < b + d

source

theorem add_lt_add_of_lt_of_le {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c d : α} (h₁ : a < b) (h₂ : c ≤ d) :

a + c < b + d

source

theorem mul_lt_mul_of_lt_of_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c d : α} (h₁ : a < b) (h₂ : c ≤ d) :

a * c < b * d

source

theorem lt_add_of_pos_right {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} (h : 0 < b) :

a < a + b

source

theorem lt_mul_of_one_lt_right' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} (h : 1 < b) :

a < a * b

source

theorem lt_add_of_pos_left {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} (h : 0 < b) :

a < b + a

source

theorem lt_mul_of_one_lt_left' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} (h : 1 < b) :

a < b * a

source

theorem le_of_mul_le_mul_right' {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (h : a * b ≤ c * b) :

a ≤ c

source

theorem le_of_add_le_add_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (h : a + b ≤ c + b) :

a ≤ c

source

theorem mul_lt_one {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (ha : a < 1) (hb : b < 1) :

a * b < 1

source

theorem add_neg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (ha : a < 0) (hb : b < 0) :

a + b < 0

source

theorem add_neg_of_neg_of_nonpos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (ha : a < 0) (hb : b ≤ 0) :

a + b < 0

source

theorem mul_lt_one_of_lt_one_of_le_one {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (ha : a < 1) (hb : b ≤ 1) :

a * b < 1

source

theorem mul_lt_one_of_le_one_of_lt_one {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (ha : a ≤ 1) (hb : b < 1) :

a * b < 1

source

theorem add_neg_of_nonpos_of_neg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (ha : a ≤ 0) (hb : b < 0) :

a + b < 0

source

theorem lt_add_of_pos_of_le {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (ha : 0 < a) (hbc : b ≤ c) :

b < a + c

source

theorem lt_mul_of_one_lt_of_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (ha : 1 < a) (hbc : b ≤ c) :

b < a * c

source

theorem lt_add_of_le_of_pos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : 0 < a) :

b < c + a

source

theorem lt_mul_of_le_of_one_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : 1 < a) :

b < c * a

source

theorem add_le_of_nonpos_of_le {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (ha : a ≤ 0) (hbc : b ≤ c) :

a + b ≤ c

source

theorem mul_le_of_le_one_of_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (ha : a ≤ 1) (hbc : b ≤ c) :

a * b ≤ c

source

theorem mul_le_of_le_of_le_one {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : a ≤ 1) :

b * a ≤ c

source

theorem add_le_of_le_of_nonpos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : a ≤ 0) :

b + a ≤ c

source

theorem mul_lt_of_lt_one_of_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (ha : a < 1) (hbc : b ≤ c) :

a * b < c

source

theorem add_lt_of_neg_of_le {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (ha : a < 0) (hbc : b ≤ c) :

a + b < c

source

theorem add_lt_of_le_of_neg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : a < 0) :

b + a < c

source

theorem mul_lt_of_le_of_lt_one {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : a < 1) :

b * a < c

source

theorem lt_mul_of_one_le_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (ha : 1 ≤ a) (hbc : b < c) :

b < a * c

source

theorem lt_add_of_nonneg_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (ha : 0 ≤ a) (hbc : b < c) :

b < a + c

source

theorem lt_mul_of_lt_of_one_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (hbc : b < c) (ha : 1 ≤ a) :

b < c * a

source

theorem lt_add_of_lt_of_nonneg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (hbc : b < c) (ha : 0 ≤ a) :

b < c + a

source

theorem lt_mul_of_one_lt_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (ha : 1 < a) (hbc : b < c) :

b < a * c

source

theorem lt_add_of_pos_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (ha : 0 < a) (hbc : b < c) :

b < a + c

source

theorem lt_mul_of_lt_of_one_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (hbc : b < c) (ha : 1 < a) :

b < c * a

source

theorem lt_add_of_lt_of_pos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (hbc : b < c) (ha : 0 < a) :

b < c + a

source

theorem mul_lt_of_le_one_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (ha : a ≤ 1) (hbc : b < c) :

a * b < c

source

theorem add_lt_of_nonpos_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (ha : a ≤ 0) (hbc : b < c) :

a + b < c

source

theorem add_lt_of_lt_of_nonpos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (hbc : b < c) (ha : a ≤ 0) :

b + a < c

source

theorem mul_lt_of_lt_of_le_one {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (hbc : b < c) (ha : a ≤ 1) :

b * a < c

source

theorem add_lt_of_neg_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (ha : a < 0) (hbc : b < c) :

a + b < c

source

theorem mul_lt_of_lt_one_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (ha : a < 1) (hbc : b < c) :

a * b < c

source

theorem mul_lt_of_lt_of_lt_one {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (hbc : b < c) (ha : a < 1) :

b * a < c

source

theorem add_lt_of_lt_of_neg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (hbc : b < c) (ha : a < 0) :

b + a < c

source

@[simp]

theorem mul_le_mul_iff_left {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b c : α} :

a * b ≤ a * c ↔ b ≤ c

source

@[simp]

theorem add_le_add_iff_left {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b c : α} :

a + b ≤ a + c ↔ b ≤ c

source

@[simp]

theorem mul_le_mul_iff_right {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (c : α) :

a * c ≤ b * c ↔ a ≤ b

source

@[simp]

theorem add_le_add_iff_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (c : α) :

a + c ≤ b + c ↔ a ≤ b

source

@[simp]

theorem mul_lt_mul_iff_left {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b c : α} :

a * b < a * c ↔ b < c

source

@[simp]

theorem add_lt_add_iff_left {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b c : α} :

a + b < a + c ↔ b < c

source

@[simp]

theorem mul_lt_mul_iff_right {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (c : α) :

a * c < b * c ↔ a < b

source

@[simp]

theorem add_lt_add_iff_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (c : α) :

a + c < b + c ↔ a < b

source

@[simp]

theorem le_add_iff_nonneg_right {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} :

a ≤ a + b ↔ 0 ≤ b

source

@[simp]

theorem le_mul_iff_one_le_right' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} :

a ≤ a * b ↔ 1 ≤ b

source

@[simp]

theorem le_add_iff_nonneg_left {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} :

a ≤ b + a ↔ 0 ≤ b

source

@[simp]

theorem le_mul_iff_one_le_left' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} :

a ≤ b * a ↔ 1 ≤ b

source

@[simp]

theorem lt_add_iff_pos_right {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} :

a < a + b ↔ 0 < b

source

@[simp]

theorem lt_mul_iff_one_lt_right' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} :

a < a * b ↔ 1 < b

source

@[simp]

theorem lt_add_iff_pos_left {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} :

a < b + a ↔ 0 < b

source

@[simp]

theorem lt_mul_iff_one_lt_left' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} :

a < b * a ↔ 1 < b

source

@[simp]

theorem add_le_iff_nonpos_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :

a + b ≤ b ↔ a ≤ 0

source

@[simp]

theorem mul_le_iff_le_one_left' {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} :

a * b ≤ b ↔ a ≤ 1

source

@[simp]

theorem add_le_iff_nonpos_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :

a + b ≤ a ↔ b ≤ 0

source

@[simp]

theorem mul_le_iff_le_one_right' {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} :

a * b ≤ a ↔ b ≤ 1

source

@[simp]

theorem add_lt_iff_neg_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :

a + b < b ↔ a < 0

source

@[simp]

theorem mul_lt_iff_lt_one_right' {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} :

a * b < b ↔ a < 1

source

@[simp]

theorem add_lt_iff_neg_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :

a + b < a ↔ b < 0

source

@[simp]

theorem mul_lt_iff_lt_one_left' {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} :

a * b < a ↔ b < 1

source

theorem mul_eq_one_iff_eq_one_of_one_le {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) :

a * b = 1 ↔ a = 1 ∧ b = 1

source

theorem add_eq_zero_iff_eq_zero_of_nonneg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) :

a + b = 0 ↔ a = 0 ∧ b = 0

source

def function.injective.ordered_cancel_add_comm_monoid {α : Type u} [ordered_cancel_add_comm_monoid α] {β : Type u_1} [has_zero β] [has_add β] (f : β → α) (hf : function.injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) :

ordered_cancel_add_comm_monoid β

Pullback an ordered_cancel_add_comm_monoid under an injective map.

source

def function.injective.ordered_cancel_comm_monoid {α : Type u} [ordered_cancel_comm_monoid α] {β : Type u_1} [has_one β] [has_mul β] (f : β → α) (hf : function.injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) :

ordered_cancel_comm_monoid β

Pullback an ordered_cancel_comm_monoid under an injective map.

Equations

function.injective.ordered_cancel_comm_monoid f hf one mul = {mul := left_cancel_semigroup.mul (function.injective.left_cancel_semigroup f hf mul), mul_assoc := _, mul_left_cancel := _, one := ordered_comm_monoid.one (function.injective.ordered_comm_monoid f hf one mul), one_mul := _, mul_one := _, mul_comm := _, mul_right_cancel := _, le := ordered_comm_monoid.le (function.injective.ordered_comm_monoid f hf one mul), lt := ordered_comm_monoid.lt (function.injective.ordered_comm_monoid f hf one mul), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_of_mul_le_mul_left := _}

source

theorem monotone.mul_strict_mono' {α : Type u} [ordered_cancel_comm_monoid α] {β : Type u_1} [preorder β] {f g : β → α} (hf : monotone f) (hg : strict_mono g) :

strict_mono (λ (x : β), (f x) * g x)

source

theorem monotone.add_strict_mono {α : Type u} [ordered_cancel_add_comm_monoid α] {β : Type u_1} [preorder β] {f g : β → α} (hf : monotone f) (hg : strict_mono g) :

strict_mono (λ (x : β), f x + g x)

source

theorem strict_mono.add_monotone {α : Type u} [ordered_cancel_add_comm_monoid α] {β : Type u_1} [preorder β] {f g : β → α} (hf : strict_mono f) (hg : monotone g) :

strict_mono (λ (x : β), f x + g x)

source

theorem strict_mono.mul_monotone' {α : Type u} [ordered_cancel_comm_monoid α] {β : Type u_1} [preorder β] {f g : β → α} (hf : strict_mono f) (hg : monotone g) :

strict_mono (λ (x : β), (f x) * g x)

source

theorem strict_mono.add_const {α : Type u} [ordered_cancel_add_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : strict_mono f) (c : α) :

strict_mono (λ (x : β), f x + c)

source

theorem strict_mono.mul_const' {α : Type u} [ordered_cancel_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : strict_mono f) (c : α) :

strict_mono (λ (x : β), (f x) * c)

source

theorem strict_mono.const_add {α : Type u} [ordered_cancel_add_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : strict_mono f) (c : α) :

strict_mono (λ (x : β), c + f x)

source

theorem strict_mono.const_mul' {α : Type u} [ordered_cancel_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : strict_mono f) (c : α) :

strict_mono (λ (x : β), c * f x)

source

theorem with_top.add_lt_add_iff_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : with_top α} :

a < ⊤ → (a + c < a + b ↔ c < b)

source

theorem with_bot.add_lt_add_iff_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : with_bot α} :

⊥ < a → (a + c < a + b ↔ c < b)

source

theorem with_top.add_lt_add_iff_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : with_top α} :

a < ⊤ → (c + a < b + a ↔ c < b)

source

theorem with_bot.add_lt_add_iff_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : with_bot α} :

⊥ < a → (c + a < b + a ↔ c < b)

source

theorem fn_min_mul_fn_max {α : Type u} {β : Type u_1} [linear_order α] [comm_semigroup β] (f : α → β) (n m : α) :

(f (min n m)) * f (max n m) = (f n) * f m

source

theorem fn_min_add_fn_max {α : Type u} {β : Type u_1} [linear_order α] [add_comm_semigroup β] (f : α → β) (n m : α) :

f (min n m) + f (max n m) = f n + f m

source

theorem min_add_max {α : Type u} [linear_order α] [add_comm_semigroup α] (n m : α) :

min n m + max n m = n + m

source

theorem min_mul_max {α : Type u} [linear_order α] [comm_semigroup α] (n m : α) :

(min n m) * max n m = n * m

source

@[class]

structure linear_ordered_cancel_add_comm_monoid (α : Type u) :

Type u

add : α → α → α
add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
add_left_cancel : ∀ (a b c_1 : α), a + b = a + c_1 → b = c_1
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
add_comm : ∀ (a b : α), a + b = b + a
add_right_cancel : ∀ (a b c_1 : α), a + b = c_1 + b → a = c_1
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b
le_of_add_le_add_left : ∀ (a b c_1 : α), a + b ≤ a + c_1 → b ≤ c_1
le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
decidable_le : decidable_rel has_le.le
decidable_eq : decidable_eq α
decidable_lt : decidable_rel has_lt.lt
lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1 → b < c_1

A linearly ordered cancellative additive commutative monoid is an additive commutative monoid with a decidable linear order in which addition is cancellative and monotone.

Instances

source

@[instance]

def linear_ordered_cancel_add_comm_monoid.to_ordered_cancel_add_comm_monoid (α : Type u) [s : linear_ordered_cancel_add_comm_monoid α] :

ordered_cancel_add_comm_monoid α

source

@[instance]

def linear_ordered_cancel_add_comm_monoid.to_linear_ordered_add_comm_monoid (α : Type u) [s : linear_ordered_cancel_add_comm_monoid α] :

linear_ordered_add_comm_monoid α

source

@[instance]

def linear_ordered_cancel_comm_monoid.to_linear_ordered_comm_monoid (α : Type u) [s : linear_ordered_cancel_comm_monoid α] :

linear_ordered_comm_monoid α

source

@[instance]

def linear_ordered_cancel_comm_monoid.to_ordered_cancel_comm_monoid (α : Type u) [s : linear_ordered_cancel_comm_monoid α] :

ordered_cancel_comm_monoid α

source

@[class]

structure linear_ordered_cancel_comm_monoid (α : Type u) :

Type u

mul : α → α → α
mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
mul_left_cancel : ∀ (a b c_1 : α), a * b = a * c_1 → b = c_1
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
mul_comm : ∀ (a b : α), a * b = b * a
mul_right_cancel : ∀ (a b c_1 : α), a * b = c_1 * b → a = c_1
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 * a ≤ c_1 * b
le_of_mul_le_mul_left : ∀ (a b c_1 : α), a * b ≤ a * c_1 → b ≤ c_1
le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
decidable_le : decidable_rel has_le.le
decidable_eq : decidable_eq α
decidable_lt : decidable_rel has_lt.lt
lt_of_mul_lt_mul_left : ∀ (a b c_1 : α), a * b < a * c_1 → b < c_1

A linearly ordered cancellative commutative monoid is a commutative monoid with a linear order in which multiplication is cancellative and monotone.

Instances

source

theorem min_mul_mul_left {α : Type u} [linear_ordered_cancel_comm_monoid α] (a b c : α) :

min (a * b) (a * c) = a * min b c

source

theorem min_add_add_left {α : Type u} [linear_ordered_cancel_add_comm_monoid α] (a b c : α) :

min (a + b) (a + c) = a + min b c

source

theorem min_add_add_right {α : Type u} [linear_ordered_cancel_add_comm_monoid α] (a b c : α) :

min (a + c) (b + c) = min a b + c

source

theorem min_mul_mul_right {α : Type u} [linear_ordered_cancel_comm_monoid α] (a b c : α) :

min (a * c) (b * c) = (min a b) * c

source

theorem max_add_add_left {α : Type u} [linear_ordered_cancel_add_comm_monoid α] (a b c : α) :

max (a + b) (a + c) = a + max b c

source

theorem max_mul_mul_left {α : Type u} [linear_ordered_cancel_comm_monoid α] (a b c : α) :

max (a * b) (a * c) = a * max b c

source

theorem max_mul_mul_right {α : Type u} [linear_ordered_cancel_comm_monoid α] (a b c : α) :

max (a * c) (b * c) = (max a b) * c

source

theorem max_add_add_right {α : Type u} [linear_ordered_cancel_add_comm_monoid α] (a b c : α) :

max (a + c) (b + c) = max a b + c

source

theorem min_le_add_of_nonneg_right {α : Type u} [linear_ordered_cancel_add_comm_monoid α] {a b : α} (hb : 0 ≤ b) :

min a b ≤ a + b

source

theorem min_le_mul_of_one_le_right {α : Type u} [linear_ordered_cancel_comm_monoid α] {a b : α} (hb : 1 ≤ b) :

min a b ≤ a * b

source

theorem min_le_add_of_nonneg_left {α : Type u} [linear_ordered_cancel_add_comm_monoid α] {a b : α} (ha : 0 ≤ a) :

min a b ≤ a + b

source

theorem min_le_mul_of_one_le_left {α : Type u} [linear_ordered_cancel_comm_monoid α] {a b : α} (ha : 1 ≤ a) :

min a b ≤ a * b

source

theorem max_le_mul_of_one_le {α : Type u} [linear_ordered_cancel_comm_monoid α] {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) :

max a b ≤ a * b

source

theorem max_le_add_of_nonneg {α : Type u} [linear_ordered_cancel_add_comm_monoid α] {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) :

max a b ≤ a + b

source

def function.injective.linear_ordered_cancel_comm_monoid {α : Type u} [linear_ordered_cancel_comm_monoid α] {β : Type u_1} [has_one β] [has_mul β] (f : β → α) (hf : function.injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) :

linear_ordered_cancel_comm_monoid β

Pullback a linear_ordered_cancel_comm_monoid under an injective map.

Equations