:: 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;