c > (y) == 
x:T. x c & y = f(x) T'
T,T':Type, f:(T
T'), c:Collection(T). < f(x) | x c > Collection(T') c == c(x)T:Type, x:T, c:Collection(T). x c Prop| Who Cites col map? | |
| col_map | Def < f(x) | x c > (y) == x:T. x c & y = f(x) T' |
| Thm* T,T':Type, f:(TT'), c:Collection(T). < f(x) | x c > Collection(T') | |
| col_member | Def x c == c(x) |
| Thm* T:Type, x:T, c:Collection(T). x c Prop |
| Syntax: | < f(x) | x c > | has structure: | col_map(T; T'; c; x.f(x)) |
About:
 |  |  |  |  |  |
 |  |  |  |