On the set of binary relations there exists well known set theoretic partial order . (Recall that a binary relations is a set of pairs.)
Here I will introduce an another partial order (vertical order) on the set of binary relations. (Analogously can be also introduces horizontal order, and also their intersection/conjunction rectangular order.)
Definition
Let f and g are binary relations. By definition f g iff f = g|dom f.
I will call the relation vertical order. Below I will prove that is a partial order.
Proposition. f g iff exists a set K such that f = g|K.
Proof. Direct implication is obvious. Reverse implication. Let f = g|K. Then dom f = K dom g. From this follows f = g|dom f. End of proof.
Reducing vertical order of relations to functions
For any relation p I will denote p* the corresponding function mapping an X to a set of Y. p* is defined by the following two equations:
dom p* = dom p and p*(x) = {y : (x, y) in p} for any x in dom p.
Note that dom f* = dom f.
Proposition. f = g <=> f* = g* for any binary relations f and g.
Proof. Obvious. End of proof.
Proposition. f g <=> f* g* <=> f* g*.
Proof. Obvious. End of proof.
Theorem. f g iff xdom f : f*(x) = g*(x).
Proof. It follows from the last proposition. End of proof.
Vertical order as a partial order
Proposition. f g implies f g.
Proof. Obvious. End of proof.
Theorem. is a partial order.
Proof. We need to prove reflexivity, transitivity, and antisymmetry of .
Reflexivity is obvious.
Transitivity. Let f g and g h. Then f = g|dom f = (h|dom g)|dom f = h|dom f because dom f dom g. So f h.
Antisymmetry. Let f g and g f. Then f g and g f. So f = g. End of proof.
I will denote infimum of two elements set {f, g} (where f and g are binary relations), corresponding to the vertical order of, as f g.
Theorem. Vertical order is a meet-semilattice (that is has infimum of any two binary relations).
Proof. This follows from f g <=> f* g* and that any two elements of the set of functions, whose images are sets of sets, have the infimum (namely set theoretic intersection). The operation * is a partial order isomorphism and so maps a semilattice to semilattice. Vertical infimum of two binary relations f and g can be so restored by the formula (f g)* = f* g*. End of proof..
Related theorems
About vertical order of binary relations there is an interesting theorem.
Related links