# Partial order on the set of binary relations (g = f|_{dom g})

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.