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 

2469

12 
Perm = upair + mono + func +

0

13 
consts

1806

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

0

15 

753

16 
defs

1806

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

0

20 

1806

21 
constdefs


22 
(*the identity function for A*)


23 
id :: i=>i


24 
"id(A) == (lam x:A. x)"

0

25 

1806

26 
(*onetoone functions from A to B*)


27 
inj :: [i,i]=>i


28 
"inj(A,B) == { f: A>B. ALL w:A. ALL x:A. f`w=f`x > w=x}"

0

29 

1806

30 
(*onto functions from A to B*)


31 
surj :: [i,i]=>i


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

0

33 

1806

34 
(*onetoone and onto functions*)


35 
bij :: [i,i]=>i


36 
"bij(A,B) == inj(A,B) Int surj(A,B)"

0

37 


38 
end
