Ordered monoids

This file provides the definitions of ordered monoids.

class OrderedCommMonoid (α : Type u_2) extends CommMonoid , PartialOrder : Type u_2

• 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 = x * Monoid.npow n 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

  Multiplication is monotone in an OrderedCommMonoid.

An ordered commutative monoid is a commutative monoid with a partial order such that a ≤ b → c * a ≤ c * b (multiplication is monotone)

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

• 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 = x + AddMonoid.nsmul n 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

  Addition is monotone in an OrderedAddCommMonoid.

An ordered (additive) commutative monoid is a commutative monoid with a partial order such that a ≤ b → c + a ≤ c + b (addition is monotone)

theorem OrderedAddCommMonoid.to_covariantClass_left.proof_1 (M : Type u_1) [OrderedAddCommMonoid M] : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

instance OrderedAddCommMonoid.to_covariantClass_left (M : Type u_2) [OrderedAddCommMonoid M] : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

• OrderedAddCommMonoid.to_covariantClass_left = OrderedAddCommMonoid.to_covariantClass_left.proof_1

instance OrderedCommMonoid.to_covariantClass_left (M : Type u_2) [OrderedCommMonoid M] : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

Equations

• OrderedCommMonoid.to_covariantClass_left = OrderedCommMonoid.to_covariantClass_left.proof_1

instance OrderedAddCommMonoid.to_covariantClass_right (M : Type u_2) [OrderedAddCommMonoid M] : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

• OrderedAddCommMonoid.to_covariantClass_right = OrderedAddCommMonoid.to_covariantClass_right.proof_1

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

instance OrderedCommMonoid.to_covariantClass_right (M : Type u_2) [OrderedCommMonoid M] : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

Equations

• OrderedCommMonoid.to_covariantClass_right = OrderedCommMonoid.to_covariantClass_right.proof_1

@[deprecated]

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

class LinearOrderedAddCommMonoid (α : Type u_2) extends LinearOrder , AddCommMonoid : Type u_2

• 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
• 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
• 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 = x + AddMonoid.nsmul n x
• add_comm : ∀ (a b : α), a + b = b + a
• add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b

  Addition is monotone in an OrderedAddCommMonoid.

A linearly ordered additive commutative monoid.

class LinearOrderedCommMonoid (α : Type u_2) extends LinearOrder , CommMonoid : Type u_2

• 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
• 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
• 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 = x * Monoid.npow n x
• mul_comm : ∀ (a b : α), a * b = b * a
• mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b

  Multiplication is monotone in an OrderedCommMonoid.

A linearly ordered commutative monoid.

class LinearOrderedAddCommMonoidWithTop (α : Type u_2) extends LinearOrderedAddCommMonoid , Top : Type u_2

• 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
• 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
• 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 = x + AddMonoid.nsmul n x
• add_comm : ∀ (a b : α), a + b = b + a
• add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
• top : α
• le_top : ∀ (x : α), x ≤ ⊤

  In a LinearOrderedAddCommMonoidWithTop, the ⊤ element is larger than any other element.

• top_add' : ∀ (x : α), ⊤ + x = ⊤

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

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

instance LinearOrderedAddCommMonoidWithTop.toOrderTop (α : Type u) [h : LinearOrderedAddCommMonoidWithTop α] : OrderTop α

Equations

• LinearOrderedAddCommMonoidWithTop.toOrderTop α = OrderTop.mk (_ : ∀ (x : α), x ≤ ⊤)

@[simp]

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

@[simp]

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