src/ZF/CardinalArith.thy
author lcp
Tue Jul 26 13:21:20 1994 +0200 (1994-07-26)
changeset 484 70b789956bd3
parent 467 92868dab2939
child 516 1957113f0d7d
permissions -rw-r--r--
Axiom of choice, cardinality results, etc.
     1 (*  Title: 	ZF/CardinalArith.thy
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Cardinal Arithmetic
     7 *)
     8 
     9 CardinalArith = Cardinal + OrderArith + Arith + Fin + 
    10 consts
    11 
    12   InfCard     :: "i=>o"
    13   "|*|"       :: "[i,i]=>i"       (infixl 70)
    14   "|+|"       :: "[i,i]=>i"       (infixl 65)
    15   csquare_rel :: "i=>i"
    16   jump_cardinal :: "i=>i"
    17   csucc       :: "i=>i"
    18 
    19 rules
    20 
    21   InfCard_def  "InfCard(i) == Card(i) & nat le i"
    22 
    23   cadd_def     "i |+| j == | i+j |"
    24 
    25   cmult_def    "i |*| j == | i*j |"
    26 
    27   csquare_rel_def
    28   "csquare_rel(k) == rvimage(k*k, lam z:k*k. split(%x y. <x Un y, <x,y>>, z), \
    29 \                            rmult(k,Memrel(k), k*k, 	\
    30 \                                  rmult(k,Memrel(k), k,Memrel(k))))"
    31 
    32   (*This def is more complex than Kunen's but it more easily proved to
    33     be a cardinal*)
    34   jump_cardinal_def
    35       "jump_cardinal(K) ==   \
    36 \         UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
    37 
    38   (*needed because jump_cardinal(K) might not be the successor of K*)
    39   csucc_def "csucc(K) == LEAST L. Card(L) & K<L"
    40 
    41 end