src/ZF/Perm.thy
author clasohm
Sat Dec 09 13:36:11 1995 +0100 (1995-12-09)
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab
permissions -rw-r--r--
removed quotes from consts and syntax sections
     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 
    12 Perm = ZF + "mono" +
    13 consts
    14     O    	::      [i,i]=>i      (infixr 60)
    15     id  	::      i=>i
    16     inj,surj,bij::      [i,i]=>i
    17 
    18 defs
    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