Ordered monoids

This file provides the definitions of ordered monoids.

ink

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

• Multiplication is monotone in an OrderedCommMonoid.

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

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

ink

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

• Addition is monotone in an OrderedAddCommMonoid.

  add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b

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

ink

instance OrderedAddCommMonoid.to_covariantClass_left (M : Type u_1) [inst : 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

ink

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

Equations

• (_ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1) = (_ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1)

ink

instance OrderedCommMonoid.to_covariantClass_left (M : Type u_1) [inst : 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

ink

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

Equations

• (_ : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1) = (_ : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1)

ink

instance OrderedAddCommMonoid.to_covariantClass_right (M : Type u_1) [inst : 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

ink

instance OrderedCommMonoid.to_covariantClass_right (M : Type u_1) [inst : 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

ink

theorem Add.to_covariantClass_left (M : Type u_1) [inst : Add M] [inst : PartialOrder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

ink

theorem Mul.to_covariantClass_left (M : Type u_1) [inst : Mul M] [inst : PartialOrder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1] : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

ink

theorem Add.to_covariantClass_right (M : Type u_1) [inst : Add M] [inst : PartialOrder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

ink

theorem Mul.to_covariantClass_right (M : Type u_1) [inst : Mul M] [inst : PartialOrder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

ink

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

ink

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

• Addition is monotone in an OrderedAddCommMonoid.

  add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b

A linearly ordered additive commutative monoid.

ink

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

• Multiplication is monotone in an OrderedCommMonoid.

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

A linearly ordered commutative monoid.

ink

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

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

  le_top : ∀ (x : α), x ≤ ⊤

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

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

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

ink

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

Equations

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

ink

@[simp]

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

ink

@[simp]

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