Ordered monoids #
This file provides the definitions of ordered monoids.
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≤ b → c * a ≤ c * b→ c * a ≤ c * b≤ c * b
(multiplication is monotone)
Instances
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≤ b → c + a ≤ c + b→ c + a ≤ c + b≤ c + b
(addition is monotone)
Instances
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)
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)
Addition is monotone in an
OrderedAddCommMonoid
.
A linearly ordered additive commutative monoid.
Instances
In a
LinearOrderedAddCommMonoidWithTop
, the⊤⊤
element is larger than any other element.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.`
Instances
Equations
- LinearOrderedAddCommMonoidWithTop.toOrderTop α = OrderTop.mk (_ : ∀ (x : α), x ≤ ⊤)