Order Theory/Preordered classes and poclasses
Definition (preordered class):
A preordered class is a set together with a binary relation satisfying the following axioms:
A poclass (shorthand for partially ordered class) is a preordered class such that the following additional axiom is satisfied:
- 3. (antisymmetry)
Example (subsets of the power set are ordered by inclusion):
Let be any set, and let . Then the relation on defined by
is an order on .
Definition (order homomorphism):
Let and be preordered classes. An order homomorphism from to is a class function so that for all .
Definition (isotonic class function):
Let be sets, and let be a preorder on , and a preorder on . A class function is said to be isotonic with respect to and iff is an order homomorphism from to .
Definition (antitonic class function):
Let be sets with preorders respectively. Then an antitonic class function from to with respect to the partial orders and is a class function such that
Definition (product order):
Let be a family of preordered classes. The product order on the cartesian product is the order given by