Ordered monoids

This file provides the definitions of ordered monoids.

class OrderedAddCommMonoid (α : Type u_2) extends AddCommMonoid , PartialOrder , AddMonoid , AddCommSemigroup , AddSemigroup , AddZeroClass , Zero , AddCommMagma , Add , Preorder , LE , LT : Type u_2

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

theorem OrderedAddCommMonoid.add_le_add_left {α : Type u_2} [self : OrderedAddCommMonoid α] (a : α) (b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b

class OrderedCommMonoid (α : Type u_2) extends CommMonoid , PartialOrder , Monoid , CommSemigroup , Semigroup , MulOneClass , One , CommMagma , Mul , Preorder , LE , LT : Type u_2

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

theorem OrderedCommMonoid.mul_le_mul_left {α : Type u_2} [self : OrderedCommMonoid α] (a : α) (b : α) : a ≤ b → ∀ (c : α), c * a ≤ c * b

instance OrderedCommMonoid.toMulLeftMono {α : Type u_1} [OrderedCommMonoid α] : MulLeftMono α

Equations

• ⋯ = ⋯

instance OrderedAddCommMonoid.toAddLeftMono {α : Type u_1} [OrderedAddCommMonoid α] : AddLeftMono α

Equations

• ⋯ = ⋯

theorem OrderedCommMonoid.toMulRightMono (M : Type u_2) [OrderedCommMonoid M] : MulRightMono M

theorem OrderedAddCommMonoid.toAddRightMono (M : Type u_2) [OrderedAddCommMonoid M] : AddRightMono M

class OrderedCancelAddCommMonoid (α : Type u_2) extends OrderedAddCommMonoid , AddCommMonoid , PartialOrder , AddMonoid , AddCommSemigroup , AddSemigroup , AddZeroClass , Zero , AddCommMagma , Add , Preorder , LE , LT : Type u_2

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

theorem OrderedCancelAddCommMonoid.le_of_add_le_add_left {α : Type u_2} [self : OrderedCancelAddCommMonoid α] (a : α) (b : α) (c : α) : a + b ≤ a + c → b ≤ c

class OrderedCancelCommMonoid (α : Type u_2) extends OrderedCommMonoid , CommMonoid , PartialOrder , Monoid , CommSemigroup , Semigroup , MulOneClass , One , CommMagma , Mul , Preorder , LE , LT : Type u_2

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

theorem OrderedCancelCommMonoid.le_of_mul_le_mul_left {α : Type u_2} [self : OrderedCancelCommMonoid α] (a : α) (b : α) (c : α) : a * b ≤ a * c → b ≤ c

@[instance 200]

instance OrderedCancelCommMonoid.toMulLeftReflectLE {α : Type u_1} [OrderedCancelCommMonoid α] : MulLeftReflectLE α

Equations

• ⋯ = ⋯

@[instance 200]

instance OrderedCancelAddCommMonoid.toAddLeftReflectLE {α : Type u_1} [OrderedCancelAddCommMonoid α] : AddLeftReflectLE α

Equations

• ⋯ = ⋯

instance OrderedCancelCommMonoid.toMulLeftReflectLT {α : Type u_1} [OrderedCancelCommMonoid α] : MulLeftReflectLT α

Equations

• ⋯ = ⋯

instance OrderedCancelAddCommMonoid.toAddLeftReflectLT {α : Type u_1} [OrderedCancelAddCommMonoid α] : AddLeftReflectLT α

Equations

• ⋯ = ⋯

theorem OrderedCancelCommMonoid.toMulRightReflectLT {α : Type u_1} [OrderedCancelCommMonoid α] : MulRightReflectLT α

theorem OrderedCancelAddCommMonoid.toAddRightReflectLT {α : Type u_1} [OrderedCancelAddCommMonoid α] : AddRightReflectLT α

@[instance 100]

instance OrderedCancelCommMonoid.toCancelCommMonoid {α : Type u_1} [OrderedCancelCommMonoid α] : CancelCommMonoid α

Equations

• OrderedCancelCommMonoid.toCancelCommMonoid = CancelCommMonoid.mk ⋯

@[instance 100]

instance OrderedCancelAddCommMonoid.toCancelAddCommMonoid {α : Type u_1} [OrderedCancelAddCommMonoid α] : AddCancelCommMonoid α

Equations

• OrderedCancelAddCommMonoid.toCancelAddCommMonoid = AddCancelCommMonoid.mk ⋯

class LinearOrderedAddCommMonoid (α : Type u_2) extends OrderedAddCommMonoid , LinearOrder , AddCommMonoid , PartialOrder , AddMonoid , AddCommSemigroup , AddSemigroup , AddZeroClass , Zero , AddCommMagma , Add , Min , Max , Ord , Preorder , LE , LT : Type u_2

A linearly ordered additive commutative monoid.

class LinearOrderedCommMonoid (α : Type u_2) extends OrderedCommMonoid , LinearOrder , CommMonoid , PartialOrder , Monoid , CommSemigroup , Semigroup , MulOneClass , One , CommMagma , Mul , Min , Max , Ord , Preorder , LE , LT : Type u_2

A linearly ordered commutative monoid.

class LinearOrderedCancelAddCommMonoid (α : Type u_2) extends OrderedCancelAddCommMonoid , LinearOrderedAddCommMonoid , OrderedAddCommMonoid , LinearOrder , AddCommMonoid , PartialOrder , AddMonoid , AddCommSemigroup , AddSemigroup , AddZeroClass , Zero , AddCommMagma , Add , Min , Max , Ord , Preorder , LE , LT : Type u_2

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

class LinearOrderedCancelCommMonoid (α : Type u_2) extends OrderedCancelCommMonoid , LinearOrderedCommMonoid , OrderedCommMonoid , LinearOrder , CommMonoid , PartialOrder , Monoid , CommSemigroup , Semigroup , MulOneClass , One , CommMagma , Mul , Min , Max , Ord , Preorder , LE , LT : Type u_2

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

@[simp]

theorem one_le_mul_self_iff {α : Type u_1} [LinearOrderedCommMonoid α] {a : α} : 1 ≤ a * a ↔ 1 ≤ a

@[simp]

theorem nonneg_add_self_iff {α : Type u_1} [LinearOrderedAddCommMonoid α] {a : α} : 0 ≤ a + a ↔ 0 ≤ a

@[simp]

theorem one_lt_mul_self_iff {α : Type u_1} [LinearOrderedCommMonoid α] {a : α} : 1 < a * a ↔ 1 < a

@[simp]

theorem pos_add_self_iff {α : Type u_1} [LinearOrderedAddCommMonoid α] {a : α} : 0 < a + a ↔ 0 < a

@[simp]

theorem mul_self_le_one_iff {α : Type u_1} [LinearOrderedCommMonoid α] {a : α} : a * a ≤ 1 ↔ a ≤ 1

@[simp]

theorem add_self_nonpos_iff {α : Type u_1} [LinearOrderedAddCommMonoid α] {a : α} : a + a ≤ 0 ↔ a ≤ 0

@[simp]

theorem mul_self_lt_one_iff {α : Type u_1} [LinearOrderedCommMonoid α] {a : α} : a * a < 1 ↔ a < 1

@[simp]

theorem add_self_neg_iff {α : Type u_1} [LinearOrderedAddCommMonoid α] {a : α} : a + a < 0 ↔ a < 0