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
```