# Ordered monoids #

This file provides the definitions of ordered monoids.

class OrderedAddCommMonoid (α : Type u_3) extends , :
Type u_3

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

• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + x
• add_comm : ∀ (a b : α), a + b = b + a
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b
Instances
class OrderedCommMonoid (α : Type u_3) extends , :
Type u_3

An ordered commutative monoid is a commutative monoid with a partial order such that multiplication is monotone.

• mul : ααα
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) x = * x
• mul_comm : ∀ (a b : α), a * b = b * a
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• mul_le_mul_left : ∀ (a b : α), a b∀ (c : α), c * a c * b
Instances
instance OrderedAddCommMonoid.toCovariantClassLeft {α : Type u_1} :
CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1
Equations
• =
instance OrderedCommMonoid.toCovariantClassLeft {α : Type u_1} :
CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1
Equations
• =
instance OrderedAddCommMonoid.toCovariantClassRight (M : Type u_3) :
CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x x_1
Equations
• =
instance OrderedCommMonoid.toCovariantClassRight (M : Type u_3) :
CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x x_1
Equations
• =
class OrderedCancelAddCommMonoid (α : Type u_3) extends :
Type u_3

An ordered cancellative additive commutative monoid is a partially ordered commutative additive monoid in which addition is cancellative and monotone.

• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + x
• add_comm : ∀ (a b : α), a + b = b + a
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b
• le_of_add_le_add_left : ∀ (a b c : α), a + b a + cb c
Instances
class OrderedCancelCommMonoid (α : Type u_3) extends :
Type u_3

An ordered cancellative commutative monoid is a partially ordered commutative monoid in which multiplication is cancellative and monotone.

• mul : ααα
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) x = * x
• mul_comm : ∀ (a b : α), a * b = b * a
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• mul_le_mul_left : ∀ (a b : α), a b∀ (c : α), c * a c * b
• le_of_mul_le_mul_left : ∀ (a b c : α), a * b a * cb c
Instances
instance OrderedCancelAddCommMonoid.toContravariantClassLeLeft {α : Type u_1} :
ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1
Equations
• =
instance OrderedCancelCommMonoid.toContravariantClassLeLeft {α : Type u_1} :
ContravariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1
Equations
• =
instance OrderedCancelAddCommMonoid.toContravariantClassLeft {α : Type u_1} :
ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1
Equations
• =
instance OrderedCancelCommMonoid.toContravariantClassLeft {α : Type u_1} :
ContravariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1
Equations
• =
instance OrderedCancelAddCommMonoid.toContravariantClassRight {α : Type u_1} :
ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1
Equations
• =
instance OrderedCancelCommMonoid.toContravariantClassRight {α : Type u_1} :
ContravariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1
Equations
• =
theorem OrderedCancelAddCommMonoid.toCancelAddCommMonoid.proof_1 {α : Type u_1} (a : α) (b : α) (c : α) (h : a + b = a + c) :
b = c
Equations
theorem OrderedCancelAddCommMonoid.toCancelAddCommMonoid.proof_6 {α : Type u_1} (a : α) (b : α) :
a + b = b + a
Equations
• OrderedCancelCommMonoid.toCancelCommMonoid = let __src := inst;
@[deprecated]
theorem bit0_pos {α : Type u_1} {a : α} (h : 0 < a) :
0 < bit0 a
class LinearOrderedAddCommMonoid (α : Type u_3) extends , , , :
Type u_3

A linearly ordered additive commutative monoid.

• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + x
• add_comm : ∀ (a b : α), a + b = b + a
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b
• min : ααα
• max : ααα
• compare : ααOrdering
• le_total : ∀ (a b : α), a b b a

A linear order is total.

• decidableLE : DecidableRel fun (x x_1 : α) => x x_1

In a linearly ordered type, we assume the order relations are all decidable.

• decidableEq :

In a linearly ordered type, we assume the order relations are all decidable.

• decidableLT : DecidableRel fun (x x_1 : α) => x < x_1

In a linearly ordered type, we assume the order relations are all decidable.

• min_def : ∀ (a b : α), min a b = if a b then a else b

The minimum function is equivalent to the one you get from minOfLe.

• max_def : ∀ (a b : α), max a b = if a b then b else a

The minimum function is equivalent to the one you get from maxOfLe.

• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b =

Comparison via compare is equal to the canonical comparison given decidable < and =.

Instances
class LinearOrderedCommMonoid (α : Type u_3) extends , , , :
Type u_3

A linearly ordered commutative monoid.

• mul : ααα
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) x = * x
• mul_comm : ∀ (a b : α), a * b = b * a
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• mul_le_mul_left : ∀ (a b : α), a b∀ (c : α), c * a c * b
• min : ααα
• max : ααα
• compare : ααOrdering
• le_total : ∀ (a b : α), a b b a

A linear order is total.

• decidableLE : DecidableRel fun (x x_1 : α) => x x_1

In a linearly ordered type, we assume the order relations are all decidable.

• decidableEq :

In a linearly ordered type, we assume the order relations are all decidable.

• decidableLT : DecidableRel fun (x x_1 : α) => x < x_1

In a linearly ordered type, we assume the order relations are all decidable.

• min_def : ∀ (a b : α), min a b = if a b then a else b

The minimum function is equivalent to the one you get from minOfLe.

• max_def : ∀ (a b : α), max a b = if a b then b else a

The minimum function is equivalent to the one you get from maxOfLe.

• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b =

Comparison via compare is equal to the canonical comparison given decidable < and =.

Instances
class LinearOrderedCancelAddCommMonoid (α : Type u_3) extends , , , :
Type u_3

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

• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + x
• add_comm : ∀ (a b : α), a + b = b + a
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b
• le_of_add_le_add_left : ∀ (a b c : α), a + b a + cb c
• min : ααα
• max : ααα
• compare : ααOrdering
• le_total : ∀ (a b : α), a b b a

A linear order is total.

• decidableLE : DecidableRel fun (x x_1 : α) => x x_1

In a linearly ordered type, we assume the order relations are all decidable.

• decidableEq :

In a linearly ordered type, we assume the order relations are all decidable.

• decidableLT : DecidableRel fun (x x_1 : α) => x < x_1

In a linearly ordered type, we assume the order relations are all decidable.

• min_def : ∀ (a b : α), min a b = if a b then a else b

The minimum function is equivalent to the one you get from minOfLe.

• max_def : ∀ (a b : α), max a b = if a b then b else a

The minimum function is equivalent to the one you get from maxOfLe.

• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b =

Comparison via compare is equal to the canonical comparison given decidable < and =.

Instances
class LinearOrderedCancelCommMonoid (α : Type u_3) extends , , , :
Type u_3

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

• mul : ααα
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) x = * x
• mul_comm : ∀ (a b : α), a * b = b * a
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• mul_le_mul_left : ∀ (a b : α), a b∀ (c : α), c * a c * b
• le_of_mul_le_mul_left : ∀ (a b c : α), a * b a * cb c
• min : ααα
• max : ααα
• compare : ααOrdering
• le_total : ∀ (a b : α), a b b a

A linear order is total.

• decidableLE : DecidableRel fun (x x_1 : α) => x x_1

In a linearly ordered type, we assume the order relations are all decidable.

• decidableEq :

In a linearly ordered type, we assume the order relations are all decidable.

• decidableLT : DecidableRel fun (x x_1 : α) => x < x_1

In a linearly ordered type, we assume the order relations are all decidable.

• min_def : ∀ (a b : α), min a b = if a b then a else b

The minimum function is equivalent to the one you get from minOfLe.

• max_def : ∀ (a b : α), max a b = if a b then b else a

The minimum function is equivalent to the one you get from maxOfLe.

• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b =

Comparison via compare is equal to the canonical comparison given decidable < and =.

Instances
class LinearOrderedAddCommMonoidWithTop (α : Type u_3) extends , :
Type u_3

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

• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + x
• add_comm : ∀ (a b : α), a + b = b + a
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b
• min : ααα
• max : ααα
• compare : ααOrdering
• le_total : ∀ (a b : α), a b b a
• decidableLE : DecidableRel fun (x x_1 : α) => x x_1
• decidableEq :
• decidableLT : DecidableRel fun (x x_1 : α) => x < x_1
• min_def : ∀ (a b : α), min a b = if a b then a else b
• max_def : ∀ (a b : α), max a b = if a b then b else a
• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b =
• top : α
• le_top : ∀ (a : α), a
• top_add' : ∀ (x : α), + x =

In a LinearOrderedAddCommMonoidWithTop, the ⊤ element is invariant under addition.

Instances
@[simp]
theorem top_add {α : Type u_1} (a : α) :
@[simp]
theorem add_top {α : Type u_1} (a : α) :
@[simp]
theorem nonneg_add_self_iff {α : Type u_1} {a : α} :
0 a + a 0 a
@[simp]
theorem one_le_mul_self_iff {α : Type u_1} {a : α} :
1 a * a 1 a
@[simp]
theorem pos_add_self_iff {α : Type u_1} {a : α} :
0 < a + a 0 < a
@[simp]
theorem one_lt_mul_self_iff {α : Type u_1} {a : α} :
1 < a * a 1 < a
@[simp]
theorem add_self_nonpos_iff {α : Type u_1} {a : α} :
a + a 0 a 0
@[simp]
theorem mul_self_le_one_iff {α : Type u_1} {a : α} :
a * a 1 a 1
@[simp]
theorem add_self_neg_iff {α : Type u_1} {a : α} :
a + a < 0 a < 0
@[simp]
theorem mul_self_lt_one_iff {α : Type u_1} {a : α} :
a * a < 1 a < 1