csquare_rel_def: renamed k to K
authorlcp
Fri Dec 23 16:29:04 1994 +0100 (1994-12-23)
changeset 827aa332949ce1a
parent 826 190974c664a3
child 828 03d7bfa70289
csquare_rel_def: renamed k to K
src/ZF/CardinalArith.thy
     1.1 --- a/src/ZF/CardinalArith.thy	Fri Dec 23 16:28:26 1994 +0100
     1.2 +++ b/src/ZF/CardinalArith.thy	Fri Dec 23 16:29:04 1994 +0100
     1.3 @@ -9,25 +9,26 @@
     1.4  CardinalArith = Cardinal + OrderArith + Arith + Finite + 
     1.5  consts
     1.6  
     1.7 -  InfCard     :: "i=>o"
     1.8 -  "|*|"       :: "[i,i]=>i"       (infixl 70)
     1.9 -  "|+|"       :: "[i,i]=>i"       (infixl 65)
    1.10 -  csquare_rel :: "i=>i"
    1.11 +  InfCard       :: "i=>o"
    1.12 +  "|*|"         :: "[i,i]=>i"       (infixl 70)
    1.13 +  "|+|"         :: "[i,i]=>i"       (infixl 65)
    1.14 +  csquare_rel   :: "i=>i"
    1.15    jump_cardinal :: "i=>i"
    1.16 -  csucc       :: "i=>i"
    1.17 +  csucc         :: "i=>i"
    1.18  
    1.19  defs
    1.20  
    1.21    InfCard_def  "InfCard(i) == Card(i) & nat le i"
    1.22  
    1.23 -  cadd_def     "i |+| j == | i+j |"
    1.24 +  cadd_def     "i |+| j == |i+j|"
    1.25  
    1.26 -  cmult_def    "i |*| j == | i*j |"
    1.27 +  cmult_def    "i |*| j == |i*j|"
    1.28  
    1.29    csquare_rel_def
    1.30 -  "csquare_rel(k) == rvimage(k*k, lam z:k*k. split(%x y. <x Un y, <x,y>>, z), \
    1.31 -\                            rmult(k,Memrel(k), k*k, 	\
    1.32 -\                                  rmult(k,Memrel(k), k,Memrel(k))))"
    1.33 +  "csquare_rel(K) ==   \
    1.34 +\        rvimage(K*K,   \
    1.35 +\                lam z:K*K. split(%x y. <x Un y, <x,y>>, z), \
    1.36 +\                rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))"
    1.37  
    1.38    (*This def is more complex than Kunen's but it more easily proved to
    1.39      be a cardinal*)