1196
|
1 |
(* Title: ZF/AC/AC16_WO4.thy
|
|
2 |
ID: $Id$
|
1203
|
3 |
Author: Krzysztof Grabczewski
|
1196
|
4 |
*)
|
|
5 |
|
|
6 |
AC16_WO4 = OrderType + AC16_lemmas + Cardinal_aux +
|
|
7 |
|
|
8 |
consts
|
|
9 |
|
1401
|
10 |
ww :: [i, i] => i
|
|
11 |
s_u :: [i, i, i, i] => i
|
|
12 |
MM :: [i, i, i] => i
|
|
13 |
LL :: [i, i, i] => i
|
|
14 |
GG :: [i, i, i] => i
|
1196
|
15 |
|
|
16 |
defs
|
|
17 |
|
|
18 |
ww_def "ww(x, k) == {u:Pow(x). u eqpoll k}"
|
|
19 |
|
|
20 |
s_u_def "s_u(u, t_n, k, y) == {v:t_n. u:v & k lepoll v Int y}"
|
|
21 |
|
|
22 |
MM_def "MM(t_n, k, y) == {v:t_n. k lepoll v Int y}"
|
|
23 |
|
|
24 |
LL_def "LL(t_n, k, y) == {v Int y. v:MM(t_n, k, y)}"
|
|
25 |
|
|
26 |
GG_def "GG(t_n, k, y) == lam v:LL(t_n, k, y).
|
|
27 |
(THE w. w:MM(t_n, k, y) & v <= w) - v"
|
|
28 |
|
|
29 |
end
|