My homepage | My math page | My math news | Donate for the research

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
∀*x*∈dom *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**

My homepage | My math page | My math news | Donate for the research