\begin{definition}[Definition:Disjoint Union (Set Theory)]
Let $\family {S_i}_{i \mathop \in I}$ be an $I$-indexed family of sets.
The '''disjoint union''' of $\family {S_i}_{i \mathop \in I}$ is defined as the set:
:$\ds \bigsqcup_{i \mathop \in I} S_i = \bigcup_{i \mathop \in I} \set {\tuple {x, i}: x \in S_i}$
where $\bigcup$ denotes union.
Each of the sets $S_i$ is canonically embedded in the '''disjoint union''' as the set:
:${S_i}^* = \set {\tuple {x, i}: x \in S_i}$
For distinct $i, j \in I$, the sets ${S_i}^*$ and ${S_j}^*$ are disjoint even if $S_i$ and $S_j$ are not.
If $S$ is a set such that $\forall i \in I: S_i = S$, then the '''disjoint union''' (as defined above) is equal to the cartesian product of $S$ and $I$:
:$\ds \bigsqcup_{i \mathop \in I} S = S \times I$
\end{definition}