0

1 
(* Title: ZF/perm


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


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 


12 
Perm = ZF +


13 
consts


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


15 
id :: "i=>i"


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


17 


18 
rules


19 


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


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}"


23 


24 
(*the identity function for A*)


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


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*)


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


32 


33 
(*onetoone and onto functions*)


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


35 


36 
end
