src/ZF/OrderArith.thy
changeset 1155 928a16e02f9f
parent 753 ec86863e87c8
child 1401 0c439768f45c
     1.1 --- a/src/ZF/OrderArith.thy	Thu Jun 22 12:58:39 1995 +0200
     1.2 +++ b/src/ZF/OrderArith.thy	Thu Jun 22 17:13:05 1995 +0200
     1.3 @@ -13,17 +13,17 @@
     1.4  
     1.5  defs
     1.6    (*disjoint sum of two relations; underlies ordinal addition*)
     1.7 -  radd_def "radd(A,r,B,s) == \
     1.8 -\                {z: (A+B) * (A+B).  \
     1.9 -\                    (EX x y. z = <Inl(x), Inr(y)>)   | 	 \
    1.10 -\                    (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   | 	 \
    1.11 -\                    (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"
    1.12 +  radd_def "radd(A,r,B,s) == 
    1.13 +                {z: (A+B) * (A+B).  
    1.14 +                    (EX x y. z = <Inl(x), Inr(y)>)   | 	 
    1.15 +                    (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   | 	 
    1.16 +                    (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"
    1.17  
    1.18    (*lexicographic product of two relations; underlies ordinal multiplication*)
    1.19 -  rmult_def "rmult(A,r,B,s) == \
    1.20 -\                {z: (A*B) * (A*B).  \
    1.21 -\                    EX x' y' x y. z = <<x',y'>, <x,y>> &	 \
    1.22 -\                       (<x',x>: r | (x'=x & <y',y>: s))}"
    1.23 +  rmult_def "rmult(A,r,B,s) == 
    1.24 +                {z: (A*B) * (A*B).  
    1.25 +                    EX x' y' x y. z = <<x',y'>, <x,y>> &	 
    1.26 +                       (<x',x>: r | (x'=x & <y',y>: s))}"
    1.27  
    1.28    (*inverse image of a relation*)
    1.29    rvimage_def "rvimage(A,f,r) == {z: A*A. EX x y. z = <x,y> & <f`x,f`y>: r}"