src/ZF/Perm.thy
 changeset 1806 12708740f58d parent 1478 2b8c2a7547ab child 2469 b50b8c0eec01
equal 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`