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

Let $R$ and $S$ be relations (Relation, $\operatorname{dom} R$, $\operatorname{ran} R$, $\operatorname{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) : \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) : \exists b\ ((a,b) \in R \wedge (b,c) \in S)\,\}$;
• the restriction $R \restriction 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 \restriction 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 \restriction A$ keeps the pairs of $R$ whose first coordinate lies in $A$ and discards the rest; $A$ need not be included in $\operatorname{dom} R$, and $\operatorname{dom}(R \restriction A) = \operatorname{dom} R \cap A$.