|
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 Schroeder-Bernstein Theorem
|
|
|
10 |
*)
|
|
|
11 |
|
|
124
|
12 |
Perm = ZF + "mono" +
|
|
0
|
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 |
(*one-to-one 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 |
(*one-to-one and onto functions*)
|
|
|
34 |
bij_def "bij(A,B) == inj(A,B) Int surj(A,B)"
|
|
|
35 |
|
|
|
36 |
end
|