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