c | P(x) > (x) == x c & P(x)
T:Type, c:Collection(T), Q:(T
Prop). < i c | Q(i) > Collection(T) c == c(x)T:Type, x:T, c:Collection(T). x c Prop| Who Cites col filter? | |
| col_filter | Def < x c | P(x) > (x) == x c & P(x) |
| Thm* T:Type, c:Collection(T), Q:(TProp). < i c | Q(i) > Collection(T) | |
| col_member | Def x c == c(x) |
| Thm* T:Type, x:T, c:Collection(T). x c Prop |
| Syntax: | < x c | P(x) > | has structure: | col_filter(x.P(x); c) |
About:
 |  |  |  |  |  |  |  |