src/ZF/Perm.thy
changeset 1806 12708740f58d
parent 1478 2b8c2a7547ab
child 2469 b50b8c0eec01
equal deleted inserted replaced
1805:10494d0241cd 1806:12708740f58d
     9   -- Lemmas for the Schroeder-Bernstein Theorem
     9   -- Lemmas for the Schroeder-Bernstein Theorem
    10 *)
    10 *)
    11 
    11 
    12 Perm = ZF + "mono" +
    12 Perm = ZF + "mono" +
    13 consts
    13 consts
    14     O           ::      [i,i]=>i      (infixr 60)
    14   O     :: [i,i]=>i      (infixr 60)
    15     id          ::      i=>i
       
    16     inj,surj,bij::      [i,i]=>i
       
    17 
    15 
    18 defs
    16 defs
       
    17   (*composition of relations and functions; NOT Suppes's relative product*)
       
    18   comp_def    "r O s == {xz : domain(s)*range(r) . 
       
    19                               EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
    19 
    20 
    20     (*composition of relations and functions; NOT Suppes's relative product*)
    21 constdefs
    21     comp_def    "r O s == {xz : domain(s)*range(r) . 
    22   (*the identity function for A*)
    22                                 EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
    23   id    :: i=>i
       
    24   "id(A) == (lam x:A. x)"
    23 
    25 
    24     (*the identity function for A*)
    26   (*one-to-one functions from A to B*)
    25     id_def      "id(A) == (lam x:A. x)"
    27   inj   :: [i,i]=>i
       
    28   "inj(A,B) == { f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x}"
    26 
    29 
    27     (*one-to-one functions from A to B*)
    30   (*onto functions from A to B*)
    28     inj_def      "inj(A,B) == { f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x}"
    31   surj  :: [i,i]=>i
       
    32   "surj(A,B) == { f: A->B . ALL y:B. EX x:A. f`x=y}"
    29 
    33 
    30     (*onto functions from A to B*)
    34   (*one-to-one and onto functions*)
    31     surj_def    "surj(A,B) == { f: A->B . ALL y:B. EX x:A. f`x=y}"
    35   bij   :: [i,i]=>i
    32 
    36   "bij(A,B) == inj(A,B) Int surj(A,B)"
    33     (*one-to-one and onto functions*)
       
    34     bij_def     "bij(A,B) == inj(A,B) Int surj(A,B)"
       
    35 
    37 
    36 end
    38 end