src/ZF/Cardinal.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 9683 f87c8c449018
permissions -rw-r--r--
expanded tabs
     1 (*  Title:      ZF/Cardinal.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Cardinals in Zermelo-Fraenkel Set Theory 
     7 *)
     8 
     9 Cardinal = OrderType + Fixedpt + Nat + Sum + 
    10 consts
    11   Least            :: (i=>o) => i    (binder "LEAST " 10)
    12   eqpoll, lepoll,
    13           lesspoll :: [i,i] => o     (infixl 50)
    14   cardinal         :: i=>i           ("|_|")
    15   Finite, Card     :: i=>o
    16 
    17 defs
    18 
    19   (*least ordinal operator*)
    20   Least_def     "Least(P) == THE i. Ord(i) & P(i) & (ALL j. j<i --> ~P(j))"
    21 
    22   eqpoll_def    "A eqpoll B == EX f. f: bij(A,B)"
    23 
    24   lepoll_def    "A lepoll B == EX f. f: inj(A,B)"
    25 
    26   lesspoll_def  "A lesspoll B == A lepoll B & ~(A eqpoll B)"
    27 
    28   Finite_def    "Finite(A) == EX n:nat. A eqpoll n"
    29 
    30   cardinal_def  "|A| == LEAST i. i eqpoll A"
    31 
    32   Card_def      "Card(i) == (i = |i|)"
    33 
    34 end