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