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