The inverse relation $R^{-1}$, the composite $S\circ R$, and the restriction $R\upharpoonright A$

Let $R$ and $S$ be relations (Relation, $\mathrm{dom}R$, $\mathrm{ran}R$, $\mathrm{fld}R$, and the specialisations "relation from $A$ to $B$" and "relation on $A$") and let $A$ be a set. By For relations $R$ and $S$ and a set $A$, the collections $\{(b,a):(a,b)\in R\}$, $\{(a,c):\mathrm{\exists }b((a,b)\in R\wedge (b,c)\in S)\}$ and $\{(a,b)\in R:a\in A\}$ are sets the three collections below are sets, and each is again a relation, since each of its elements is an ordered pair (The Kuratowski ordered pair $(a,b):=\{\{a\},\{a,b\}\}$):

• the inverse $R^{-1}:=\{(b,a):(a,b)\in R\}$;
• the composite $S\circ R:=\{(a,c):\mathrm{\exists }b((a,b)\in R\wedge (b,c)\in S)\}$;
• the restriction $R\upharpoonright A:=\{(a,b)\in R:a\in A\}$.

Membership in each is exactly as written: $(b,a)\in R^{-1}$ holds if and only if $(a,b)\in R$; $(a,c)\in S\circ R$ holds if and only if $(a,b)\in R$ and $(b,c)\in S$ for some $b$; and $(a,b)\in R\upharpoonright A$ holds if and only if $(a,b)\in R$ and $a\in A$.

• The order in $S\circ R$. $S\circ R$ applies $R$ first and $S$ second. This is the convention that makes the composite of functions read $(g\circ f)(x)=g(f(x))$, and it is the one the rest of the library uses. The opposite convention exists in the literature and would reverse every composite written here.

• Restriction cuts the domain, not the range. $R\upharpoonright A$ keeps the pairs of $R$ whose first coordinate lies in $A$ and discards the rest; $A$ need not be included in $\mathrm{dom}R$, and $\mathrm{dom}(R\upharpoonright A)=\mathrm{dom}R\cap A$.