Thm* P:(T![](FONT/dash.png) Prop), c1,c2:Collection(T).
c1 = c2 ![](FONT/eq.png) (( x c1.P(x)) ![](FONT/if_big.png) ( x c2.P(x))) | [col_all_functionality] |
Thm* c:Collection(T), P:(T![](FONT/dash.png) Prop). ( x c.P(x)) ![](FONT/if_big.png) ( x:T. x c ![](FONT/eq.png) P(x)) | [col_all_iff] |
Thm* l:Collection(T) List, x:T List.
x col_list_prod(l) ![](FONT/if_big.png) ||x|| = ||l|| & ( i: . i < ||x|| ![](FONT/eq.png) x[i] l[i]) | [member_col_list_prod] |
Thm* c:Collection(T), f:(T![](FONT/dash.png) Collection(T')), y:T'.
y ( x c.f(x)) ![](FONT/if_big.png) ( x:T. x c & y f(x)) | [member_col_accum] |
Thm* a,b:Collection(T), x:T. x a + b ![](FONT/if_big.png) x a x b | [member_col_add] |
Thm* c:Collection(T), f:(T![](FONT/dash.png) T'), x:T'.
x < f(y) | y c > ![](FONT/if_big.png) ( y:T. y c & x = f(y)) | [member_col_map] |
Thm* C:(I![](FONT/dash.png) Collection(T)), x:T. x i:I. C(i) ![](FONT/if_big.png) ( i:I. x C(i)) | [member_col_union] |
Thm* c1:Collection(T). c1 c1 | [col_le_reflexive] |
Thm* f:(T![](FONT/dash.png) Prop), c:Collection(T), x:T. x < i c | f(i) > ![](FONT/if_big.png) x c & f(x) | [member_col_filter] |
Thm* a1,b1,a2,b2:Collection(T).
a1 = b1 ![](FONT/eq.png) a2 = b2 ![](FONT/eq.png) (a1 = a2 ![](FONT/if_big.png) b1 = b2) | [col_equal_functionality] |
Thm* a,b,c:Collection(T). a b ![](FONT/eq.png) b c ![](FONT/eq.png) a c | [col_le_transitivity] |
Thm* c1,c2:Collection(T). c1 = c2 ![](FONT/eq.png) c1 c2 | [col_le_weakening] |
Thm* c:Collection(T). < > c | [col_none_le] |
Thm* c1,c2:Collection(T), t1,t2:T.
t1 = t2 ![](FONT/eq.png) c1 = c2 ![](FONT/eq.png) (t1 c1 ![](FONT/if_big.png) t2 c2) | [col_member_functionality] |
Thm* c1,c2,c3:Collection(T). c1 = c2 ![](FONT/eq.png) c2 = c3 ![](FONT/eq.png) c1 = c3 | [col_equal_transitivity] |
Thm* c1,c2:Collection(T). c1 = c2 ![](FONT/eq.png) c2 = c1 | [col_equal_inversion] |
Thm* c1,c2:Collection(T). c1 = c2 ![](FONT/eq.png) c1 = c2 | [col_equal_weakening] |
Thm* T:Type{i'}, x:T. x < > ![](FONT/if_big.png) False | [member_col_none] |
Def ( x c.P(x)) == x:T. x c ![](FONT/eq.png) P(x) | [col_all] |
Def col_list_prod(l)(x) == ||x|| = ||l|| & ( i: . i < ||x|| ![](FONT/eq.png) x[i] l[i]) | [col_list_prod] |
Def c1 c2 == x:T. x c1 ![](FONT/eq.png) x c2 | [col_le] |
Def c1 = c2 == x:T. x c1 ![](FONT/if_big.png) x c2 | [col_equal] |