Ordered monoids

This file provides the definitions of ordered monoids.

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

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

• add : α → α → α
• 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 : α), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b

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

class OrderedCommMonoid (α : Type u_3) extends CommMonoid , PartialOrder : 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 : α), Monoid.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Monoid.npow (n + 1) x = Monoid.npow n 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b

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

instance OrderedAddCommMonoid.toCovariantClassLeft {α : Type u_1} [OrderedAddCommMonoid α] : CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1

Equations

• ⋯ = ⋯

instance OrderedCommMonoid.toCovariantClassLeft {α : Type u_1} [OrderedCommMonoid α] : CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1

Equations

• ⋯ = ⋯

theorem OrderedAddCommMonoid.toCovariantClassRight (M : Type u_3) [OrderedAddCommMonoid M] : CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1

theorem OrderedCommMonoid.toCovariantClassRight (M : Type u_3) [OrderedCommMonoid M] : CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1

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

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

• add : α → α → α
• 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 : α), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = 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 + c → b ≤ c

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

class OrderedCancelCommMonoid (α : Type u_3) extends OrderedCommMonoid : 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 : α), Monoid.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Monoid.npow (n + 1) x = Monoid.npow n 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = 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 * c → b ≤ c

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

@[instance 200]

instance OrderedCancelAddCommMonoid.toContravariantClassLeLeft {α : Type u_1} [OrderedCancelAddCommMonoid α] : ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1

Equations

• ⋯ = ⋯

@[instance 200]

instance OrderedCancelCommMonoid.toContravariantClassLeLeft {α : Type u_1} [OrderedCancelCommMonoid α] : ContravariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1

Equations

• ⋯ = ⋯

instance OrderedCancelAddCommMonoid.toContravariantClassLeft {α : Type u_1} [OrderedCancelAddCommMonoid α] : ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1

Equations

• ⋯ = ⋯

instance OrderedCancelCommMonoid.toContravariantClassLeft {α : Type u_1} [OrderedCancelCommMonoid α] : ContravariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1

Equations

• ⋯ = ⋯

theorem OrderedCancelAddCommMonoid.toContravariantClassRight {α : Type u_1} [OrderedCancelAddCommMonoid α] : ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1

theorem OrderedCancelCommMonoid.toContravariantClassRight {α : Type u_1} [OrderedCancelCommMonoid α] : ContravariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1

theorem OrderedCancelAddCommMonoid.toCancelAddCommMonoid.proof_4 {α : Type u_1} [OrderedCancelAddCommMonoid α] (x : α) : AddMonoid.nsmul 0 x = 0

theorem OrderedCancelAddCommMonoid.toCancelAddCommMonoid.proof_2 {α : Type u_1} [OrderedCancelAddCommMonoid α] (a : α) : 0 + a = a

@[instance 100]

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

Equations

• OrderedCancelAddCommMonoid.toCancelAddCommMonoid = let __src := inst; AddCancelCommMonoid.mk ⋯

theorem OrderedCancelAddCommMonoid.toCancelAddCommMonoid.proof_3 {α : Type u_1} [OrderedCancelAddCommMonoid α] (a : α) : a + 0 = a

theorem OrderedCancelAddCommMonoid.toCancelAddCommMonoid.proof_6 {α : Type u_1} [OrderedCancelAddCommMonoid α] (a : α) (b : α) : a + b = b + a

theorem OrderedCancelAddCommMonoid.toCancelAddCommMonoid.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] (a : α) (b : α) (c : α) (h : a + b = a + c) : b = c

theorem OrderedCancelAddCommMonoid.toCancelAddCommMonoid.proof_5 {α : Type u_1} [OrderedCancelAddCommMonoid α] (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x

@[instance 100]

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

Equations

• OrderedCancelCommMonoid.toCancelCommMonoid = let __src := inst; CancelCommMonoid.mk ⋯

class LinearOrderedAddCommMonoid (α : Type u_3) extends OrderedAddCommMonoid , Min , Max , Ord : Type u_3

A linearly ordered additive commutative monoid.

• add : α → α → α
• 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 : α), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = 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 : 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 = compareOfLessAndEq a b

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

class LinearOrderedCommMonoid (α : Type u_3) extends OrderedCommMonoid , Min , Max , Ord : 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 : α), Monoid.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Monoid.npow (n + 1) x = Monoid.npow n 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = 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 : 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 = compareOfLessAndEq a b

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

class LinearOrderedCancelAddCommMonoid (α : Type u_3) extends OrderedCancelAddCommMonoid , Min , Max , Ord : 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 : α → α → α
• 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 : α), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = 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 + c → b ≤ 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 : 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 = compareOfLessAndEq a b

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

class LinearOrderedCancelCommMonoid (α : Type u_3) extends OrderedCancelCommMonoid , Min , Max , Ord : 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 : α), Monoid.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Monoid.npow (n + 1) x = Monoid.npow n 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = 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 * c → b ≤ 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 : 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 = compareOfLessAndEq a b

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

class LinearOrderedAddCommMonoidWithTop (α : Type u_3) extends LinearOrderedAddCommMonoid , OrderTop : Type u_3

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

• add : α → α → α
• 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 : α), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = 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 : 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 = compareOfLessAndEq a b
• top : α
• le_top : ∀ (a : α), a ≤ ⊤
• top_add' : ∀ (x : α), ⊤ + x = ⊤

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

theorem LinearOrderedAddCommMonoidWithTop.top_add' {α : Type u_3} [self : LinearOrderedAddCommMonoidWithTop α] (x : α) : ⊤ + x = ⊤

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

@[simp]

theorem top_add {α : Type u_1} [LinearOrderedAddCommMonoidWithTop α] (a : α) : ⊤ + a = ⊤

@[simp]

theorem add_top {α : Type u_1} [LinearOrderedAddCommMonoidWithTop α] (a : α) : a + ⊤ = ⊤

@[simp]

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

@[simp]

theorem one_le_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 one_lt_mul_self_iff {α : Type u_1} [LinearOrderedCommMonoid α] {a : α} : 1 < a * a ↔ 1 < a

@[simp]

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

@[simp]

theorem mul_self_le_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

@[simp]

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