i:I. C(i))(x) == 
i:I. x 
C(i)
T,I:Type, C:(I
Collection(T)). (i:I. C(i)) Collection(T) c == c(x)T:Type, x:T, c:Collection(T). x c Prop| Who Cites col union? | |
| col_union | Def (i:I. C(i))(x) == i:I. x C(i) |
| Thm* T,I:Type, C:(ICollection(T)). (i:I. C(i)) Collection(T) | |
| col_member | Def x c == c(x) |
| Thm* T:Type, x:T, c:Collection(T). x c Prop |
| Syntax: | i:I. C(i) | has structure: | col_union(I; i.C(i)) |
About:
 |  |  |  |  |  |  |  |