Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Countable Sets and Hessenberg's Theorem

**by****Grzegorz Bancerek**- Received September 5, 1990
- MML identifier: CARD_4

- [ Mizar article, MML identifier index ]

environ vocabulary ORDINAL1, CARD_1, FUNCT_1, FINSET_1, TARSKI, ORDINAL2, BOOLE, RELAT_1, CARD_2, ZFMISC_1, GROUP_1, ARYTM_3, MCART_1, FINSEQ_2, FINSEQ_1, PROB_1, RLVECT_1, FUNCOP_1, CARD_3, FUNCT_2, PARTFUN1, FUNCT_4, CARD_4, HAHNBAN; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSET_1, ORDINAL1, WELLORD2, ORDINAL2, MCART_1, DOMAIN_1, CARD_1, CARD_2, FINSEQ_2, FUNCT_2, FUNCT_4, FUNCOP_1, PARTFUN1, NEWTON, PROB_1, CARD_3; constructors NAT_1, WELLORD2, DOMAIN_1, CARD_2, FUNCT_4, FUNCOP_1, PARTFUN1, NEWTON, CARD_3, PROB_1, MEMBERED, XBOOLE_0; clusters SUBSET_1, FUNCT_1, FINSEQ_1, ORDINAL1, CARD_1, CARD_3, FINSET_1, FINSEQ_2, RELSET_1, NAT_1, XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin reserve X,Y,Z,x,y,y1,y2 for set, D for non empty set, k,m,n,n1,n2,n3,m2,m1 for Nat, A,B for Ordinal, L,K,M,N for Cardinal, f,g for Function; theorem :: CARD_4:1 X is finite iff Card X is finite; theorem :: CARD_4:2 X is finite iff Card X <` alef 0; theorem :: CARD_4:3 X is finite implies Card X in alef 0 & Card X in omega; theorem :: CARD_4:4 X is finite iff ex n st Card X = Card n; theorem :: CARD_4:5 succ A \ {A} = A; theorem :: CARD_4:6 A,n are_equipotent implies A = n; theorem :: CARD_4:7 A is finite iff A in omega; theorem :: CARD_4:8 not A is finite iff omega c= A; theorem :: CARD_4:9 M is finite iff M in alef 0; canceled; theorem :: CARD_4:11 not M is finite iff alef 0 c= M; canceled; theorem :: CARD_4:13 N is finite & not M is finite implies N <` M & N <=` M; theorem :: CARD_4:14 not X is finite iff ex Y st Y c= X & Card Y = alef 0; theorem :: CARD_4:15 not omega is finite & not NAT is finite; theorem :: CARD_4:16 not alef 0 is finite; theorem :: CARD_4:17 X = {} iff Card X = 0; canceled; theorem :: CARD_4:19 0 <=` M; theorem :: CARD_4:20 Card X = Card Y iff nextcard X = nextcard Y; theorem :: CARD_4:21 M = N iff nextcard N = nextcard M; theorem :: CARD_4:22 N <` M iff nextcard N <=` M; theorem :: CARD_4:23 N <` nextcard M iff N <=` M; theorem :: CARD_4:24 0 <` M iff 1 <=` M; theorem :: CARD_4:25 1 <` M iff 2 <=` M; theorem :: CARD_4:26 M is finite & (N <=` M or N <` M) implies N is finite; theorem :: CARD_4:27 A is_limit_ordinal iff for B,n st B in A holds B+^ n in A; theorem :: CARD_4:28 A+^succ n = succ A +^ n & A +^ (n+1) = succ A +^ n; theorem :: CARD_4:29 ex n st A*^succ one = A +^ n; theorem :: CARD_4:30 A is_limit_ordinal implies A *^ succ one = A; theorem :: CARD_4:31 omega c= A implies one+^A = A; theorem :: CARD_4:32 M is infinite implies M is_limit_ordinal; theorem :: CARD_4:33 not M is finite implies M+`M = M; theorem :: CARD_4:34 not M is finite & (N <=` M or N <` M) implies M+`N = M & N+`M = M; theorem :: CARD_4:35 not X is finite & (X,Y are_equipotent or Y,X are_equipotent) implies X \/ Y,X are_equipotent & Card (X \/ Y) = Card X; theorem :: CARD_4:36 not X is finite & Y is finite implies X \/ Y,X are_equipotent & Card (X \/ Y) = Card X; theorem :: CARD_4:37 not X is finite & (Card Y <` Card X or Card Y <=` Card X) implies X \/ Y,X are_equipotent & Card (X \/ Y) = Card X; theorem :: CARD_4:38 for M,N being finite Cardinal holds M+`N is finite; theorem :: CARD_4:39 not M is finite implies not M+`N is finite & not N+`M is finite; theorem :: CARD_4:40 for M,N being finite Cardinal holds M*`N is finite; theorem :: CARD_4:41 K <` L & M <` N or K <=` L & M <` N or K <` L & M <=` N or K <=` L & M <=` N implies K+`M <=` L+`N & M+`K <=` L+`N; theorem :: CARD_4:42 M <` N or M <=` N implies K+`M <=` K+`N & K+`M <=` N+`K & M+`K <=` K+`N & M+`K <=` N+`K; definition let X; attr X is countable means :: CARD_4:def 1 Card X <=` alef 0; end; theorem :: CARD_4:43 X is finite implies X is countable; theorem :: CARD_4:44 omega is countable & NAT is countable; theorem :: CARD_4:45 X is countable iff ex f st dom f = NAT & X c= rng f; theorem :: CARD_4:46 Y c= X & X is countable implies Y is countable; theorem :: CARD_4:47 X is countable & Y is countable implies X \/ Y is countable; theorem :: CARD_4:48 X is countable implies X /\ Y is countable & Y /\ X is countable; theorem :: CARD_4:49 X is countable implies X \ Y is countable; theorem :: CARD_4:50 X is countable & Y is countable implies X \+\ Y is countable; reserve r for Real; theorem :: CARD_4:51 r <> 0 or n = 0 iff r|^n <> 0; definition let m,n be Nat; redefine func m|^n -> Nat; end; theorem :: CARD_4:52 (2|^n1)*(2*m1+1) = (2|^n2)*(2*m2+1) implies n1 = n2 & m1 = m2; theorem :: CARD_4:53 [:NAT,NAT:],NAT are_equipotent & Card NAT = Card [:NAT,NAT:]; theorem :: CARD_4:54 (alef 0)*`(alef 0) = alef 0; theorem :: CARD_4:55 X is countable & Y is countable implies [:X,Y:] is countable; theorem :: CARD_4:56 1-tuples_on D,D are_equipotent & Card (1-tuples_on D) = Card D; reserve p,q for FinSequence; theorem :: CARD_4:57 [:n-tuples_on D, m-tuples_on D:],(n+m)-tuples_on D are_equipotent & Card [:n-tuples_on D, m-tuples_on D:] = Card ((n+m)-tuples_on D); theorem :: CARD_4:58 D is countable implies n-tuples_on D is countable; theorem :: CARD_4:59 (Card dom f <=` M & for x st x in dom f holds Card (f.x) <=` N) implies Card Union f <=` M*`N; theorem :: CARD_4:60 (Card X <=` M & for Y st Y in X holds Card Y <=` N) implies Card union X <=` M*`N; theorem :: CARD_4:61 for f st dom f is countable & for x st x in dom f holds f.x is countable holds Union f is countable; theorem :: CARD_4:62 (X is countable & for Y st Y in X holds Y is countable) implies union X is countable; theorem :: CARD_4:63 for f st dom f is finite & for x st x in dom f holds f.x is finite holds Union f is finite; canceled; theorem :: CARD_4:65 D is countable implies D* is countable; theorem :: CARD_4:66 alef 0 <=` Card (D*); scheme FraenCoun1 { f(set)->set, P[Nat] } : { f(n) : P[n] } is countable; scheme FraenCoun2 { f(set,set)->set, P[set,set] } : { f(n1,n2) : P[n1,n2] } is countable; scheme FraenCoun3 { f(set,set,set)->set, P[Nat,Nat,Nat] } : { f(n1,n2,n3) : P[n1,n2,n3] } is countable; theorem :: CARD_4:67 (alef 0)*`(Card n) <=` alef 0 & (Card n)*`(alef 0) <=` alef 0; theorem :: CARD_4:68 K <` L & M <` N or K <=` L & M <` N or K <` L & M <=` N or K <=` L & M <=` N implies K*`M <=` L*`N & M*`K <=` L*`N; theorem :: CARD_4:69 M <` N or M <=` N implies K*`M <=` K*`N & K*`M <=` N*`K & M*`K <=` K*`N & M*`K <=` N*`K; theorem :: CARD_4:70 K <` L & M <` N or K <=` L & M <` N or K <` L & M <=` N or K <=` L & M <=` N implies K = 0 or exp(K,M) <=` exp(L,N); theorem :: CARD_4:71 M <` N or M <=` N implies K = 0 or exp(K,M) <=` exp(K,N) & exp(M,K) <=` exp(N,K); theorem :: CARD_4:72 M <=` M+`N & N <=` M+`N; theorem :: CARD_4:73 N <> 0 implies M <=` M*`N & M <=` N*`M; theorem :: CARD_4:74 K <` L & M <` N implies K+`M <` L+`N & M+`K <` L+`N; theorem :: CARD_4:75 K+`M <` K+`N implies M <` N; theorem :: CARD_4:76 Card X +` Card Y = Card X & Card Y <` Card X implies Card (X \ Y) = Card X; reserve f,f1,f2 for Function, X1,X2 for set; :: Hessenberg's theorem theorem :: CARD_4:77 not M is finite implies M*`M = M; theorem :: CARD_4:78 not M is finite & 0 <` N & (N <=` M or N <` M) implies M*`N = M & N*`M = M; theorem :: CARD_4:79 not M is finite & (N <=` M or N <` M) implies M*`N <=` M & N*`M <=` M; theorem :: CARD_4:80 not X is finite implies [:X,X:],X are_equipotent & Card [:X,X:] = Card X; theorem :: CARD_4:81 not X is finite & Y is finite & Y <> {} implies [:X,Y:],X are_equipotent & Card [:X,Y:] = Card X; theorem :: CARD_4:82 K <` L & M <` N implies K*`M <` L*`N & M*`K <` L*`N; theorem :: CARD_4:83 K*`M <` K*`N implies M <` N; theorem :: CARD_4:84 not X is finite implies Card X = (alef 0)*`Card X; theorem :: CARD_4:85 X <> {} & X is finite & not Y is finite implies Card Y *` Card X = Card Y; theorem :: CARD_4:86 not D is finite & n <> 0 implies n-tuples_on D,D are_equipotent & Card (n-tuples_on D) = Card D; theorem :: CARD_4:87 not D is finite implies Card D = Card (D*);

Back to top