**This theorem has appeared wrong.** There is a counterexample (formulated in this news message). It seems that I’ve mistaken in the following phrase “what accordingly noted above is equivalent to *gg*^{-1} = *fg*^{-1}.” There seems no thing noted above accordingly which would be *gg*^{-1} = *fg*^{-1}.

The counterexample:

*f* = N^{2}; *g* = {(*n*,*m*) in N^{2} | *n* less or equal than *m*} where N is the set of natural numbers.

In this example *gg*^{-1} = *fg*^{-1} = N^{2} but not *g* = *f*|_{dom g} because *f*|_{dom g} = *f*.

**Theorem.** Let *f* and *g* are binary relations. Then the following statements are equivalent:

*g*=*f*|_{dom g}.- Exists a set
*K*such that*g*=*f*|_{K}. *gg*^{-1}=*fg*^{-1}and*g*is a subset of*f*.*gg*^{-1}=*gf*^{-1}and*g*is a subset of*f*.*gg*^{-1}=*fg*^{-1}and dom*g*is a subset of dom*f*.*gg*^{-1}=*gf*^{-1}and dom*g*is a subset of dom*f*.

An other, a little less convenient for usage but much easier to remember (mnemonic), equivalent form of this theorem is:

**Theorem (mnemonic form).** Given that *f* and *g* are binary relations and dom *g* is a subset of dom *f*, right multiplying

(composing) both sides of the equation *g* = *f*|_{dom g} with *g*^{-1} produces a formula equivalent to this equation.

I have stated this theorem as a conjecture in this weblog post. Now I have proved it. (The proof is below.)

Note that *qp* denotes the composition of binary relations *p* and *q*.

**Lemma**

First we will prove the following lemma:

**Lemma.** If *gg*^{-1} = *fg*^{-1} and dom *g* is a subset of dom *f* then *f*|_{dom g} = *g* for any binary relations *f* and *g*.

**Proof.** Let *gg*^{-1} = *fg*^{-1}.

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*.

I will denote L the multivalued function (relation) which maps a set to its elements (that is the reverse of set membership relation). Obviously *p* = L*p** and *p* = *q* <=> *p** = *q** for any relations *p* and *q*.

Our equation can be equivalently rewritten as L*g**(L*g**)^{-1} = L*f**(L*g**)^{-1}; L*g***g**^{-1}L^{-1} = L*f***g**^{-1}L^{-1}; what accordingly noted above is equivalent to *g***g**^{-1} = *f***g**^{-1}.

By well known properties of monovalued functions, we have *g***g**^{-1} = I_{im g*} (I_{im g*} denotes the identity relation on the set im *g**); so *f***g**^{-1} = I_{im g*}, that is for any *y* in im *g** we have *f***g**^{-1}*y* = *y*.

So for any *x* in dom *g** we have *f***g**^{-1}*g***x* = *g***x*. Because *g**^{-1}*g***x* contains *x* and *x* in dom *f** (dom *f** is a superset of dom *g**), we have *f***x* = *g***x*.

So *f**|_{dom g*} = *g** what is the same as *f*|_{dom g} = *g*. **End of proof.**

**Proof of the main theorem**

Now we can easily prove the main theorem. First we will prove its mnemonic form (repeated below):

**Theorem (mnemonic form).** Given that *f* and *g* are binary relations and dom *g* is a subset of dom *f*, right multiplying both sides of the equation *g* = *f*|_{dom g} with *g*^{-1} produces a formula equivalent to this equation.

**Proof of the main theorem (mnemonic form).**

Multiplying both sides of the equation *g* = *f*|_{dom g} with *g*^{-1} produces the formula *gg*^{-1} = *fg*^{-1}. We need to prove that this formula is equivalent to *g* = *f*|_{dom g} (under the condition that dom *g* is a subset of dom *f*).

Direct implication is obvious. Reverse implication is already proved in the lemma (that dom *g* is a subset of dom *f* is taken into account). **End of proof**.

Now let reprise the full form of the main theorem again and prove it:

**Theorem.** Let *f* and *g* are binary relations. Then the following statements are equivalent:

*g*=*f*|_{dom g}.- Exists a set
*K*such that*g*=*f*|_{K}. *gg*^{-1}=*fg*^{-1}and*g*is a subset of*f*.*gg*^{-1}=*gf*^{-1}and*g*is a subset of*f*.*gg*^{-1}=*fg*^{-1}and dom*g*is a subset of dom*f*.*gg*^{-1}=*gf*^{-1}and dom*g*is a subset of dom*f*.

**Proof of the main theorem (full form).**

Equivalences (3)<=>(4) and (5)<=>(6) can be proved by inverting the formulas taking in account that (*qp*)^{-1} = *p*^{-1}*q*^{-1} for any binary relations *p* and *q*.

Implications (3)=>(5) and (4)=>(6) are obvious.

(5)=>(1) is exactly the lemma proved above.

(1)=>(3) is obvious (right multiply both sides of the equality (1) with *g*^{-1}).

(1)=>(2) is obvious. (Take *K* = dom *g*.)

To prove (2)=>(1) let assume that *g* = *f*|_{K}. Then dom *g* is intersection of dom *f* and the set *K*; from this follows *g* = *f*|_{dom g}.

From proved implications follows that all six statements are equivalent. **End of proof.**

**Name and authorship of the theorem**

I do not remember that I would have seen this theorem anywhere else. Maybe I am the first who found this theorem (in the start of November 2005)? If so let this theorem be called *the theorem of Porton about limiting binary relations* or simply *the theorem about limiting binary relations*.

**Related links**

- Homepage of this theorem.
- Definition of vertical order of binary relations (a partial order).
- This theorem is used in my category theory research, particularly the theory of dependencies.