1478

1 
(* Title: ZF/perm

0

2 
ID: $Id$

1478

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

0

4 
Copyright 1991 University of Cambridge


5 


6 
The theory underlying permutation groups


7 
 Composition of relations, the identity relation


8 
 Injections, surjections, bijections


9 
 Lemmas for the SchroederBernstein Theorem


10 
*)


11 

124

12 
Perm = ZF + "mono" +

0

13 
consts

1478

14 
O :: [i,i]=>i (infixr 60)


15 
id :: i=>i

1401

16 
inj,surj,bij:: [i,i]=>i

0

17 

753

18 
defs

0

19 


20 
(*composition of relations and functions; NOT Suppes's relative product*)

1478

21 
comp_def "r O s == {xz : domain(s)*range(r) .


22 
EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"

0

23 


24 
(*the identity function for A*)

1478

25 
id_def "id(A) == (lam x:A. x)"

0

26 


27 
(*onetoone 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}"


29 


30 
(*onto functions from A to B*)

1478

31 
surj_def "surj(A,B) == { f: A>B . ALL y:B. EX x:A. f`x=y}"

0

32 


33 
(*onetoone and onto functions*)

1478

34 
bij_def "bij(A,B) == inj(A,B) Int surj(A,B)"

0

35 


36 
end
