Order Theory/Preordered classes and poclasses

Definition (preordered class):

A preordered class is a set together with a binary relation satisfying the following axioms:

  1. (reflexivity)
  2. (transitivity)

Definition (poclass):

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