:: K\"onig's Theorem :: by Grzegorz Bancerek :: :: Received April 10, 1990 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies ORDINAL1, CARD_1, SUBSET_1, FUNCT_1, RELAT_1, FUNCOP_1, XBOOLE_0, ZFMISC_1, TARSKI, FUNCT_2, MCART_1, FINSET_1, NAT_1, WELLORD1, WELLORD2, RELAT_2, SETFAM_1, PARTFUN1, FUNCT_4, CARD_3, PBOOLE, NAGATA_1; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, CARD_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, SETFAM_1, ORDINAL1, WELLORD1, MCART_1, WELLORD2, FUNCOP_1, FUNCT_4, FINSET_1, FINSUB_1, PBOOLE; constructors SETFAM_1, RELAT_2, WELLORD1, PARTFUN1, WELLORD2, FUNCOP_1, FUNCT_4, CLASSES1, ORDINAL2, ORDINAL3, FINSET_1, CARD_1, FINSUB_1, RELSET_1, FUNCT_1, PBOOLE, XTUPLE_0; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FUNCT_4, FINSET_1, CARD_1, PBOOLE, RELSET_1, XTUPLE_0; requirements BOOLE, SUBSET; begin reserve A,B,C for Ordinal, K,L,M,N for Cardinal, x,y,y1,y2,z,u for object,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; registration cluster empty -> Cardinal-yielding for Function; end; registration cluster Cardinal-yielding for Function; end; definition mode Cardinal-Function is Cardinal-yielding Function; end; reserve ff for Cardinal-Function; registration let ff,X; cluster ff|X -> Cardinal-yielding; end; registration let X,K; cluster X --> K -> Cardinal-yielding; end; registration let X be object; let K; cluster X .--> K -> Cardinal-yielding; end; scheme :: CARD_3:sch 1 CFLambda { A()->set, F(object)->Cardinal } : ex ff st dom ff = A() & for x being set 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 being object st x in dom f holds it.x = [:f.x,{x}:]; func Union f -> set equals :: CARD_3:def 4 union rng f; func product f -> set means :: CARD_3:def 5 for x being object holds x in it iff ex g st x = g & dom g = dom f & for y being object st y in dom f holds g.y in f.y; end; theorem :: CARD_3:1 Card ff = ff; theorem :: CARD_3:2 Card (X --> Y) = X --> card Y; theorem :: CARD_3:3 disjoin {} = {}; theorem :: CARD_3:4 disjoin (x .--> X) = x .--> [:X,{x}:]; theorem :: CARD_3:5 x in dom f & y in dom f & x <> y implies (disjoin f).x misses (disjoin f).y; theorem :: CARD_3:6 Union (X --> Y) c= Y; theorem :: CARD_3:7 X <> {} implies Union (X --> Y) = Y; theorem :: CARD_3:8 Union (x .--> Y) = Y; theorem :: CARD_3:9 g in product f iff dom g = dom f & for x being object st x in dom f holds g.x in f.x; theorem :: CARD_3:10 product {} = {{}}; theorem :: CARD_3:11 Funcs(X,Y) = product (X --> Y); definition let x be object; let X; func pi(X,x) -> set means :: CARD_3:def 6 for y being object holds y in it iff ex f st f in X & y = f.x; end; theorem :: CARD_3:12 x in dom f & product f <> {} implies pi(product f,x) = f.x; theorem :: CARD_3:13 pi({},x) = {}; theorem :: CARD_3:14 pi({g},x) = {g.x}; theorem :: CARD_3:15 pi({f,g},x) = {f.x,g.x}; theorem :: CARD_3:16 pi(X \/ Y,x) = pi(X,x) \/ pi(Y,x); theorem :: CARD_3:17 pi(X /\ Y,x) c= pi(X,x) /\ pi(Y,x); theorem :: CARD_3:18 pi(X,x) \ pi(Y,x) c= pi(X \ Y,x); theorem :: CARD_3:19 pi(X,x) \+\ pi(Y,x) c= pi(X \+\ Y,x); theorem :: CARD_3:20 card pi(X,x) c= card X; theorem :: CARD_3:21 x in Union disjoin f implies ex y,z being object st x = [y,z]; theorem :: CARD_3:22 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:23 f c= g implies disjoin f c= disjoin g; theorem :: CARD_3:24 f c= g implies Union f c= Union g; theorem :: CARD_3:25 Union disjoin (Y --> X) = [:X,Y:]; theorem :: CARD_3:26 product f = {} iff {} in rng f; theorem :: CARD_3:27 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:28 for x st x in dom F holds card (F.x) = F.x; theorem :: CARD_3:29 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; theorem :: CARD_3:30 dom F = dom G & (for x st x in dom F holds F.x c= G.x) implies Sum F c= Sum G; theorem :: CARD_3:31 {} in rng F iff Product F = 0; theorem :: CARD_3:32 dom F = dom G & (for x st x in dom F holds F.x c= G.x) implies Product F c= Product G; theorem :: CARD_3:33 F c= G implies Sum F c= Sum G; theorem :: CARD_3:34 F c= G & not 0 in rng G implies Product F c= Product G; theorem :: CARD_3:35 Sum({} --> K) = 0; theorem :: CARD_3:36 Product ({} --> K) = 1; theorem :: CARD_3:37 Sum(x .--> K) = K; theorem :: CARD_3:38 Product(x .--> K) = K; theorem :: CARD_3:39 card Union f c= Sum Card f; theorem :: CARD_3:40 card Union F c= Sum F; ::$N Koenig Theorem theorem :: CARD_3:41 dom F = dom G & (for x st x in dom F holds F.x in G.x) implies Sum F in Product G; scheme :: CARD_3:sch 2 FuncSeparation { X()->set, F(object)->set, P[object,object] }: ex f st dom f = X() & for x being object st x in X() for y being object holds y in f.x iff y in F(x) & P[x,y]; theorem :: CARD_3:42 X is finite implies card X in card omega; theorem :: CARD_3:43 card A in card B implies A in B; theorem :: CARD_3:44 card A in M implies A in M; theorem :: CARD_3:45 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:46 (for Z st Z in X holds card Z in M) & X is c=-linear implies card union X c= M; begin :: Addenda :: from AMI_1 registration let f be Function; cluster product f -> functional; end; registration let A be set; let B be with_non-empty_elements set; cluster -> non-empty for Function of A,B; end; :: from PRVECT_1 registration let f be non-empty Function; cluster product f -> non empty; end; :: from AMI_1, 2006.03.14, A.T. theorem :: CARD_3:47 for a,b,c,d being set st a <> b holds product (a,b) --> ({c},{d}) = { (a,b) --> (c,d) }; :: from AMI_1, 2006.03.14, A.T. theorem :: CARD_3:48 x in product f implies x is Function; begin :: Superproducts, from AMI_1, 2006.03.14, A.T. reserve A,B for set; definition let f be Function; func sproduct f -> set means :: CARD_3:def 9 for x being object holds x in it iff ex g st x = g & dom g c= dom f & for x being object st x in dom g holds g.x in f.x; end; registration let f be Function; cluster sproduct f -> functional non empty; end; theorem :: CARD_3:49 g in sproduct f implies dom g c= dom f & for x st x in dom g holds g.x in f.x; theorem :: CARD_3:50 {} in sproduct f; registration let f; cluster empty for Element of sproduct f; end; theorem :: CARD_3:51 product f c= sproduct f; theorem :: CARD_3:52 x in sproduct f implies x is PartFunc of dom f, union rng f; theorem :: CARD_3:53 g in product f & h in sproduct f implies g +* h in product f; theorem :: CARD_3:54 product f <> {} implies (g in sproduct f iff ex h st h in product f & g c= h); theorem :: CARD_3:55 sproduct f c= PFuncs(dom f,union rng f); theorem :: CARD_3:56 f c= g implies sproduct f c= sproduct g; theorem :: CARD_3:57 sproduct {} = {{}}; theorem :: CARD_3:58 PFuncs(A,B) = sproduct (A --> B); theorem :: CARD_3:59 for A, B being non empty set for f being Function of A,B holds sproduct f = sproduct(f|{x where x is Element of A: f.x <> {} }); theorem :: CARD_3:60 x in dom f & y in f.x implies x .--> y in sproduct f; theorem :: CARD_3:61 sproduct f = {{}} iff for x st x in dom f holds f.x = {}; theorem :: CARD_3:62 A c= sproduct f & (for h1,h2 being Function st h1 in A & h2 in A holds h1 tolerates h2) implies union A in sproduct f; theorem :: CARD_3:63 g tolerates h & g in sproduct f & h in sproduct f implies g \/ h in sproduct f; theorem :: CARD_3:64 for x being set holds x c= h & h in sproduct f implies x in sproduct f; theorem :: CARD_3:65 g in sproduct f implies g|A in sproduct f; theorem :: CARD_3:66 g in sproduct f implies g|A in sproduct f|A; theorem :: CARD_3:67 h in sproduct(f+*g) implies ex f9,g9 being Function st f9 in sproduct f & g9 in sproduct g & h = f9+*g9; theorem :: CARD_3:68 for f9,g9 being Function st dom g misses dom f9 \ dom g9 & f9 in sproduct f & g9 in sproduct g holds f9+*g9 in sproduct(f+*g); theorem :: CARD_3:69 for f9,g9 being Function st dom f9 misses dom g \ dom g9 & f9 in sproduct f & g9 in sproduct g holds f9+*g9 in sproduct(f+*g); theorem :: CARD_3:70 g in sproduct f & h in sproduct f implies g +* h in sproduct f; theorem :: CARD_3:71 for x1,x2,y1,y2 being set holds x1 in dom f & y1 in f.x1 & x2 in dom f & y2 in f.x2 implies (x1,x2)-->(y1,y2) in sproduct f; begin :: from PRALG_2, 2007.11.14, A.T. definition let IT be set; attr IT is with_common_domain means :: CARD_3:def 10 for f,g be Function st f in IT & g in IT holds dom f = dom g; end; registration cluster with_common_domain functional non empty for set; end; registration let f; cluster {f} -> with_common_domain; end; definition let X be functional set; func DOM X -> set equals :: CARD_3:def 11 meet the set of all dom f where f is Element of X; end; theorem :: CARD_3:72 for X be with_common_domain functional set st X = {{}} holds DOM X = {}; registration let X be empty set; cluster DOM X -> empty; end; begin :: Product like sets, from AMISTD_2, 2007.11.14, A.T. definition let S be functional set; func product" S -> Function means :: CARD_3:def 12 :: tu trzeba uzyc DOM dom it = DOM S & for i being set st i in dom it holds it.i = pi(S,i); end; ::$CT theorem :: CARD_3:74 for S being non empty functional set, i being set st i in dom product" S holds (product" S).i = the set of all f.i where f is Element of S; definition let S be set; attr S is product-like means :: CARD_3:def 13 ex f being Function st S = product f; end; registration let f be Function; cluster product f -> product-like; end; registration cluster product-like -> functional with_common_domain for set; end; registration cluster product-like non empty for set; end; ::$CT 2 theorem :: CARD_3:77 for S being functional with_common_domain set holds S c= product product" S; theorem :: CARD_3:78 for S being non empty product-like set holds S = product product" S; :: from AMI_1, 2008.04.11, A.T. (generalized) theorem :: CARD_3:79 for f being Function for s, t being Element of product f, A be set holds s +* t|A is Element of product f; theorem :: CARD_3:80 for f being non-empty Function for p being Element of sproduct f ex s being Element of product f st p c= s; theorem :: CARD_3:81 g in product f implies g|A in sproduct f; :: needed, 2008.04.20, A.T. definition let f be non-empty Function; let g be Element of product f; let X; redefine func g|X -> Element of sproduct f; end; theorem :: CARD_3:82 for f being non-empty Function for s,ss being Element of product f, A being set holds (ss +* s | A) | A = s | A; :: from PRE_CIRC, 2008.06.02, A.T. theorem :: CARD_3:83 for M,x, g being Function st x in product M holds x * g in product (M * g); :: moved from CARD_4, 2008.10.08, A.T. theorem :: CARD_3:84 X is finite iff card X in omega; reserve A,B for Ordinal; theorem :: CARD_3:85 A is infinite iff omega c= A; theorem :: CARD_3:86 N is finite & not M is finite implies N in M & N c= M; theorem :: CARD_3:87 not X is finite iff ex Y st Y c= X & card Y = omega; theorem :: CARD_3:88 card X = card Y iff nextcard X = nextcard Y; theorem :: CARD_3:89 nextcard N = nextcard M implies M = N; theorem :: CARD_3:90 N in M iff nextcard N c= M; theorem :: CARD_3:91 N in nextcard M iff N c= M; theorem :: CARD_3:92 M is finite & (N c= M or N in M) implies N is finite; reserve n,k for Nat; definition let X; attr X is countable means :: CARD_3:def 14 card X c= omega; attr X is denumerable means :: CARD_3:def 15 card X = omega; end; registration cluster denumerable -> countable infinite for set; cluster countable infinite -> denumerable for set; end; registration cluster finite -> countable for set; end; registration cluster omega -> denumerable; end; registration cluster denumerable for set; end; theorem :: CARD_3:93 X is countable iff ex f st dom f = omega & X c= rng f; registration let X be countable set; cluster -> countable for Subset of X; end; theorem :: CARD_3:94 X is countable implies X /\ Y is countable; theorem :: CARD_3:95 X is countable implies X \ Y is countable; theorem :: CARD_3:96 for A being non empty countable set ex f being Function of omega, A st rng f = A; :: from CIRCCOMB, 2009.01.26, A.T. theorem :: CARD_3:97 for f,g being non-empty Function, x being Element of product f, y being Element of product g holds x+*y in product (f+*g); theorem :: CARD_3:98 for f,g being non-empty Function for x being Element of product (f+*g) holds x|dom g in product g; theorem :: CARD_3:99 for f,g being non-empty Function st f tolerates g for x being Element of product (f+*g) holds x|dom f in product f; :: missing, 2009.09.06, A.T. theorem :: CARD_3:100 for S being with_common_domain functional set, f be Function st f in S holds dom f = dom product" S; theorem :: CARD_3:101 for S being functional set, f be Function, i be set st f in S & i in dom product" S holds f.i in (product" S).i; theorem :: CARD_3:102 for S being with_common_domain functional set, f be Function, i be set st f in S & i in dom f holds f.i in (product" S).i; :: 2009.09.12, A.T. registration let X be with_common_domain set; cluster -> with_common_domain for Subset of X; end; :: from PRALG_3, 2009.09.18, A.T. definition let f be Function, x be object; func proj(f,x) -> Function means :: CARD_3:def 16 dom it = product f & for y being Function st y in dom it holds it.y = y.x; end; registration let f be Function, x be object; cluster proj(f,x) -> (product f)-defined; end; registration let f be Function, x be object; cluster proj(f,x) -> total; end; registration let f be non-empty Function; cluster -> f-compatible for Element of product f; end; registration let I be set; let f be I-defined non-empty Function; cluster -> I-defined for Element of product f; end; registration let f be Function; cluster -> f-compatible for Element of sproduct f; end; registration let I be set; let f be I-defined Function; cluster -> I-defined for Element of sproduct f; end; registration let I be set; let f be total I-defined non-empty Function; cluster -> total for Element of product f; end; theorem :: CARD_3:103 for I being set, f being non-empty I-defined Function for p being f-compatible I-defined Function holds p in sproduct f; theorem :: CARD_3:104 for I being set, f being non-empty I-defined Function for p being f-compatible I-defined Function ex s being Element of product f st p c= s; :: from AMISTD_2, 2010.01.10, A.T registration let X be infinite set, a be set; cluster X --> a -> infinite; end; registration cluster infinite for Function; end; registration let R be infinite Relation; cluster field R -> infinite; end; registration let X be infinite set; cluster RelIncl X -> infinite; end; theorem :: CARD_3:105 for R,S being Relation st R,S are_isomorphic & R is finite holds S is finite; theorem :: CARD_3:106 product" {{}} = {}; theorem :: CARD_3:107 for I being set, f being non-empty ManySortedSet of I for s being f-compatible ManySortedSet of I holds s in product f; registration let I be set, f be non-empty ManySortedSet of I; cluster -> total for Element of product f; end; definition let I be set, f be non-empty ManySortedSet of I; let M be f-compatible ManySortedSet of I; func down M -> Element of product f equals :: CARD_3:def 17 M; end; theorem :: CARD_3:108 for X being functional with_common_domain set for f being Function st f in X holds dom f = DOM X; theorem :: CARD_3:109 for x being object, X being non empty functional set st for f being Function st f in X holds x in dom f holds x in DOM X; scheme :: CARD_3:sch 3 FuncSepOrg { X()->set, F(object)->set, P[object,object] }: ex f st dom f = X() & for x being set st x in X() for y being set holds y in f.x iff y in F(x) & P[x,y]; :: from NAGATA_1, 2013.01.13, A.T. notation let X be set; antonym X is uncountable for X is countable; end; registration cluster uncountable -> non empty for set; end;