Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### K\"onig's Theorem

**by****Grzegorz Bancerek**- Received April 10, 1990
- MML identifier: CARD_3

- [ Mizar article, MML identifier index ]

environ vocabulary ORDINAL1, CARD_1, FUNCT_1, RELAT_1, BOOLE, FUNCOP_1, FUNCT_2, TARSKI, MCART_1, PROB_1, RLVECT_1, CARD_2, ORDINAL2, FINSET_1, ARYTM_1, CLASSES1, ZFMISC_1, WELLORD1, WELLORD2, RELAT_2, CARD_3, HAHNBAN; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, REAL_1, NAT_1, RELAT_1, RELAT_2, FUNCT_1, FUNCT_2, ORDINAL1, WELLORD1, MCART_1, WELLORD2, CARD_1, FUNCOP_1, FUNCT_4, FINSET_1, PROB_1, CARD_2, CLASSES1; constructors REAL_1, NAT_1, RELAT_2, WELLORD1, MCART_1, WELLORD2, FUNCOP_1, PROB_1, CARD_2, CLASSES1, MEMBERED, XBOOLE_0; clusters RELAT_1, FUNCT_1, FINSET_1, CARD_1, FUNCOP_1, ORDINAL1, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2; requirements NUMERALS, BOOLE, SUBSET; begin reserve A,B,C for Ordinal, K,M,N for Cardinal, x,y,y1,y2,z,u,X,Y,Z,Z1,Z2 for set, n for Nat, f,f1,g,h for Function, Q,R for Relation; definition let IT be Function; attr IT is Cardinal-yielding means :: CARD_3:def 1 for x st x in dom IT holds IT.x is Cardinal; end; definition cluster Cardinal-yielding Function; end; definition mode Cardinal-Function is Cardinal-yielding Function; end; reserve ff for Cardinal-Function; definition let ff,X; cluster ff|X -> Cardinal-yielding; end; definition let X,K; cluster X --> K -> Cardinal-yielding; end; canceled 2; theorem :: CARD_3:3 {} is Cardinal-Function; scheme CF_Lambda { A()->set, F(set)->Cardinal } : ex ff st dom ff = A() & for x st x in A() holds ff.x = F(x); definition let f; func Card f -> Cardinal-Function means :: CARD_3:def 2 dom it = dom f & for x st x in dom f holds it.x = Card(f.x); func disjoin f -> Function means :: CARD_3:def 3 dom it = dom f & for x st x in dom f holds it.x = [:f.x,{x}:]; canceled; func product f -> set means :: CARD_3:def 5 x in it iff ex g st x = g & dom g = dom f & for y st y in dom f holds g.y in f.y; end; canceled 4; theorem :: CARD_3:8 Card ff = ff; theorem :: CARD_3:9 Card {} = {}; theorem :: CARD_3:10 Card (X --> Y) = X --> Card Y; theorem :: CARD_3:11 disjoin {} = {}; theorem :: CARD_3:12 disjoin ({x} --> X) = {x} --> [:X,{x}:]; theorem :: CARD_3:13 x in dom f & y in dom f & x <> y implies (disjoin f).x misses (disjoin f).y; theorem :: CARD_3:14 Union {} = {}; theorem :: CARD_3:15 Union (X --> Y) c= Y; theorem :: CARD_3:16 X <> {} implies Union (X --> Y) = Y; theorem :: CARD_3:17 Union ({x} --> Y) = Y; theorem :: CARD_3:18 g in product f iff dom g = dom f & for x st x in dom f holds g.x in f.x; theorem :: CARD_3:19 product {} = {{}}; theorem :: CARD_3:20 Funcs(X,Y) = product (X --> Y); definition let x,X; func pi(X,x) -> set means :: CARD_3:def 6 y in it iff ex f st f in X & y = f.x; end; canceled; theorem :: CARD_3:22 x in dom f & product f <> {} implies pi(product f,x) = f.x; canceled; theorem :: CARD_3:24 pi({},x) = {}; theorem :: CARD_3:25 pi({g},x) = {g.x}; theorem :: CARD_3:26 pi({f,g},x) = {f.x,g.x}; theorem :: CARD_3:27 pi(X \/ Y,x) = pi(X,x) \/ pi(Y,x); theorem :: CARD_3:28 pi(X /\ Y,x) c= pi(X,x) /\ pi(Y,x); theorem :: CARD_3:29 pi(X,x) \ pi(Y,x) c= pi(X \ Y,x); theorem :: CARD_3:30 pi(X,x) \+\ pi(Y,x) c= pi(X \+\ Y,x); theorem :: CARD_3:31 Card pi(X,x) <=` Card X; theorem :: CARD_3:32 x in Union disjoin f implies ex y,z st x = [y,z]; theorem :: CARD_3:33 x in Union disjoin f iff x`2 in dom f & x`1 in f.(x`2) & x = [x`1,x`2]; theorem :: CARD_3:34 f <= g implies disjoin f <= disjoin g; theorem :: CARD_3:35 f <= g implies Union f c= Union g; theorem :: CARD_3:36 Union disjoin (Y --> X) = [:X,Y:]; theorem :: CARD_3:37 product f = {} iff {} in rng f; theorem :: CARD_3:38 dom f = dom g & (for x st x in dom f holds f.x c= g.x) implies product f c= product g; reserve F,G for Cardinal-Function; theorem :: CARD_3:39 for x st x in dom F holds Card (F.x) = F.x; theorem :: CARD_3:40 for x st x in dom F holds Card ((disjoin F).x) = F.x; definition let F; func Sum F -> Cardinal equals :: CARD_3:def 7 Card Union disjoin F; func Product F -> Cardinal equals :: CARD_3:def 8 Card product F; end; canceled 2; theorem :: CARD_3:43 dom F = dom G & (for x st x in dom F holds F.x c= G.x) implies Sum F <=` Sum G; theorem :: CARD_3:44 {} in rng F iff Product F = 0; theorem :: CARD_3:45 dom F = dom G & (for x st x in dom F holds F.x c= G.x) implies Product F <=` Product G; theorem :: CARD_3:46 F <= G implies Sum F <=` Sum G; theorem :: CARD_3:47 F <= G & not 0 in rng G implies Product F <=` Product G; theorem :: CARD_3:48 Sum({} --> K) = 0; theorem :: CARD_3:49 Product ({} --> K) = 1; theorem :: CARD_3:50 Sum({x} --> K) = K; theorem :: CARD_3:51 Product({x} --> K) = K; theorem :: CARD_3:52 Sum(M --> N) = M*`N; theorem :: CARD_3:53 Product(N --> M) = exp(M,N); theorem :: CARD_3:54 Card Union f <=` Sum Card f; theorem :: CARD_3:55 Card Union F <=` Sum F; :: :: K\"onig's theorem :: theorem :: CARD_3:56 dom F = dom G & (for x st x in dom F holds F.x in G.x) implies Sum F <` Product G; scheme FinRegularity { X()->finite set, P[set,set] }: ex x st x in X() & for y st y in X() & y <> x holds not P[y,x] provided X() <> {} and for x,y st P[x,y] & P[y,x] holds x = y and for x,y,z st P[x,y] & P[y,z] holds P[x,z]; scheme MaxFinSetElem { X()->finite set, P[set,set] }: ex x st x in X() & for y st y in X() holds P[x,y] provided X() <> {} and for x,y holds P[x,y] or P[y,x] and for x,y,z st P[x,y] & P[y,z] holds P[x,z]; scheme FuncSeparation { X()->set, F(set)->set, P[set,set] }: ex f st dom f = X() & for x st x in X() for y holds y in f.x iff y in F(x) & P[x,y]; theorem :: CARD_3:57 Rank n is finite; theorem :: CARD_3:58 X is finite implies Card X <` Card omega; theorem :: CARD_3:59 Card A <` Card B implies A in B; theorem :: CARD_3:60 Card A <` M implies A in M; theorem :: CARD_3:61 X is c=-linear implies ex Y st Y c= X & union Y = union X & for Z st Z c= Y & Z <> {} ex Z1 st Z1 in Z & for Z2 st Z2 in Z holds Z1 c= Z2; theorem :: CARD_3:62 (for Z st Z in X holds Card Z <` M) & X is c=-linear implies Card union X <=` M;

Back to top