src/ZF/AC/AC16_WO4.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 5284 c77e9dd9bafc
permissions -rw-r--r--
expanded tabs
clasohm@1478
     1
(*  Title:      ZF/AC/AC16_WO4.thy
lcp@1196
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Krzysztof Grabczewski
lcp@1196
     4
*)
lcp@1196
     5
lcp@1196
     6
AC16_WO4 = OrderType + AC16_lemmas + Cardinal_aux +
lcp@1196
     7
lcp@1196
     8
consts
lcp@1196
     9
clasohm@1401
    10
  ww  :: [i, i] => i
clasohm@1401
    11
  s_u :: [i, i, i, i] => i
clasohm@1401
    12
  MM  :: [i, i, i] => i
clasohm@1401
    13
  LL  :: [i, i, i] => i
clasohm@1401
    14
  GG  :: [i, i, i] => i
lcp@1196
    15
  
lcp@1196
    16
defs
lcp@1196
    17
lcp@1196
    18
  ww_def  "ww(x, k) == {u:Pow(x). u eqpoll k}"
lcp@1196
    19
lcp@1196
    20
  s_u_def "s_u(u, t_n, k, y) == {v:t_n. u:v & k lepoll v Int y}"
lcp@1196
    21
lcp@1196
    22
  MM_def  "MM(t_n, k, y) == {v:t_n. k lepoll v Int y}"
lcp@1196
    23
lcp@1196
    24
  LL_def  "LL(t_n, k, y) == {v Int y. v:MM(t_n, k, y)}"
lcp@1196
    25
lcp@1196
    26
  GG_def  "GG(t_n, k, y) == lam v:LL(t_n, k, y). 
clasohm@1478
    27
                            (THE w. w:MM(t_n, k, y) & v <= w) - v"
lcp@1196
    28
lcp@1196
    29
end