Cover

Set

context $X$
definiendum $C$ in it
postulate $f:I\to C$
postulate $X \subseteq \bigcup_{i\in I,\ f}C_i$

Discussion

where we have some indexing via a set $I$.

Parents

Requirements

Indexed union