Indexed union
Set
| context | $f:I\to X$ |
| definiendum | $\bigcup_{i\in I,\ f} X_i \equiv \bigcup \mathrm{im}(f)$ |
Discussion
For $f=\mathrm{id}$, the set is indexing itself and the indexed union is just the arbitrary union $\bigcup_{i\in I} X_i = \bigcup X$.
Parents
Refinement of
Context
