Composition

🅟 Feb 21, 2026

  🅤 Mar 07, 2026

DEF-CP. Composition.

Let $R$ and $S$ be binary relations. The composition of $R$ and $S$ is the relation

\[S\circ R = \{(x,z):(\exists y:x\,R\,y\land y\,S\,z)\}.\]

$S\circ R$ is a set:

\[S\circ R \subseteq \dom R\times\ran S.\]

PROP-CP-ID.

  1. For any binary relation $R$,

    \[R\circ\id_{\dom R} = \id_{\ran R}\circ R = R.\]
  2. For any binary relation $R$ on $X$,

    \[R\circ\id_X = \id_X\circ R = R.\]

PROP-CP-ASS. Associativity.

For any binary relations $R$, $S$ and $T$,

\[(R\circ S)\circ T = R\circ(S\circ T).\]

PROP-CP-F.

If $f$ and $g$ are functions on $X$, then $f\circ g$ is also a function on $X$.

As results:

PROP-CP-MO.

For any set $X$, $(\powerset(X\times X),\circ)$ is a monoid with neutral element $\id_X$.

PROP-CP-FMO.

For any set $X$, $\fun(X,X)$ is a submonoid of $\powerset(X\times X)$ with neutral element $\id_X$.


PROP-CP-CV.

For any binary relations $R$ and $S$,

\[(R\circ S)^{-1} = S^{-1}\circ R^{-1}.\]