7.3.10 Products of Families of Relations
Let $\webleft\{ A_{i}\webright\} _{i\in I}$ and $\webleft\{ B_{i}\webright\} _{i\in I}$ be families of sets, and let $\webleft\{ R_{i}\colon A_{i}\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B_{i}\webright\} _{i\in I}$ be a family of relations.
The product of the family $\webleft\{ R_{i}\webright\} _{i\in I}$ is the relation $\smash {\prod _{i\in I}R_{i}}$ from $\smash {\prod _{i\in I}A_{i}}$ to $\smash {\prod _{i\in I}B_{i}}$ defined as follows:
- Viewing relations as subsets, we define $\smash {\prod _{i\in I}R_{i}}$ as its product as a family of sets, i.e. we have
\[ \prod _{i\in I}R_{i} \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ \webleft (a_{i},b_{i}\webright )_{i\in I}\in \prod _{i\in I}\webleft (A_{i}\times B_{i}\webright )\ \middle |\ \begin{aligned} & \text{for each $i\in I$,}\\ & \text{we have $a_{i}\sim _{R_{i}}b_{i}$}\end{aligned} \webright\} . \]
- Viewing relations as functions to powersets, we define
\[ \webleft[\prod _{i\in I}R_{i}\webright]\webleft (\webleft (a_{i}\webright )_{i\in I}\webright ) \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\prod _{i\in I}R_{i}\webleft (a_{i}\webright ) \]
for each $\webleft (a_{i}\webright )_{i\in I}\in \prod _{i\in I}R_{i}$.