:: K\"onig's Theorem
:: by Grzegorz Bancerek
::
:: Received April 10, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines Cardinal-yielding CARD_3:def 1 :
theorem :: CARD_3:1
canceled;
theorem :: CARD_3:2
canceled;
theorem :: CARD_3:3
:: deftheorem Def2 defines Card CARD_3:def 2 :
:: deftheorem Def3 defines disjoin CARD_3:def 3 :
:: deftheorem defines Union CARD_3:def 4 :
:: deftheorem Def5 defines product CARD_3:def 5 :
theorem :: CARD_3:4
canceled;
theorem :: CARD_3:5
canceled;
theorem :: CARD_3:6
canceled;
theorem :: CARD_3:7
canceled;
theorem Th8: :: CARD_3:8
theorem :: CARD_3:9
theorem :: CARD_3:10
theorem :: CARD_3:11
theorem Th12: :: CARD_3:12
theorem :: CARD_3:13
theorem :: CARD_3:14
canceled;
theorem Th15: :: CARD_3:15
theorem Th16: :: CARD_3:16
theorem :: CARD_3:17
theorem Th18: :: CARD_3:18
theorem Th19: :: CARD_3:19
theorem Th20: :: CARD_3:20
defpred S1[ set ] means $1 is Function;
:: deftheorem Def6 defines pi CARD_3:def 6 :
for
x,
X,
b3 being
set holds
(
b3 = pi X,
x iff for
y being
set holds
(
y in b3 iff ex
f being
Function st
(
f in X &
y = f . x ) ) );
theorem :: CARD_3:21
canceled;
theorem :: CARD_3:22
theorem :: CARD_3:23
canceled;
theorem :: CARD_3:24
theorem :: CARD_3:25
theorem :: CARD_3:26
theorem Th27: :: CARD_3:27
theorem :: CARD_3:28
theorem Th29: :: CARD_3:29
theorem :: CARD_3:30
theorem Th31: :: CARD_3:31
theorem Th32: :: CARD_3:32
theorem Th33: :: CARD_3:33
theorem Th34: :: CARD_3:34
theorem Th35: :: CARD_3:35
theorem Th36: :: CARD_3:36
theorem Th37: :: CARD_3:37
theorem Th38: :: CARD_3:38
theorem :: CARD_3:39
theorem Th40: :: CARD_3:40
:: deftheorem defines Sum CARD_3:def 7 :
:: deftheorem defines Product CARD_3:def 8 :
theorem :: CARD_3:41
canceled;
theorem :: CARD_3:42
canceled;
theorem Th43: :: CARD_3:43
theorem :: CARD_3:44
theorem :: CARD_3:45
theorem :: CARD_3:46
theorem :: CARD_3:47
theorem :: CARD_3:48
theorem :: CARD_3:49
theorem :: CARD_3:50
theorem :: CARD_3:51
theorem :: CARD_3:52
theorem :: CARD_3:53
theorem Th54: :: CARD_3:54
theorem :: CARD_3:55
theorem :: CARD_3:56
scheme :: CARD_3:sch 2
FinRegularity{
F1()
-> finite set ,
P1[
set ,
set ] } :
ex
x being
set st
(
x in F1() & ( for
y being
set st
y in F1() &
y <> x holds
not
P1[
y,
x] ) )
provided
A1:
F1()
<> {}
and A2:
for
x,
y being
set st
P1[
x,
y] &
P1[
y,
x] holds
x = y
and A3:
for
x,
y,
z being
set st
P1[
x,
y] &
P1[
y,
z] holds
P1[
x,
z]
scheme :: CARD_3:sch 3
MaxFinSetElem{
F1()
-> finite set ,
P1[
set ,
set ] } :
ex
x being
set st
(
x in F1() & ( for
y being
set st
y in F1() holds
P1[
x,
y] ) )
provided
A1:
F1()
<> {}
and A2:
for
x,
y being
set holds
(
P1[
x,
y] or
P1[
y,
x] )
and A3:
for
x,
y,
z being
set st
P1[
x,
y] &
P1[
y,
z] holds
P1[
x,
z]
Lm1:
for n being Element of NAT st Rank n is finite holds
Rank (n + 1) is finite
theorem :: CARD_3:57
Lm2:
for x being set
for R being Relation st x in field R holds
ex y being set st
( [x,y] in R or [y,x] in R )
theorem Th58: :: CARD_3:58
theorem Th59: :: CARD_3:59
theorem Th60: :: CARD_3:60
theorem Th61: :: CARD_3:61
theorem :: CARD_3:62
theorem :: CARD_3:63
theorem :: CARD_3:64
:: deftheorem Def9 defines sproduct CARD_3:def 9 :
theorem Th65: :: CARD_3:65
theorem Th66: :: CARD_3:66
theorem Th67: :: CARD_3:67
theorem Th68: :: CARD_3:68
theorem Th69: :: CARD_3:69
theorem :: CARD_3:70
theorem Th71: :: CARD_3:71
theorem Th72: :: CARD_3:72
theorem Th73: :: CARD_3:73
theorem :: CARD_3:74
theorem :: CARD_3:75
theorem Th76: :: CARD_3:76
theorem :: CARD_3:77
theorem Th78: :: CARD_3:78
theorem :: CARD_3:79
theorem Th80: :: CARD_3:80
theorem Th81: :: CARD_3:81
theorem Th82: :: CARD_3:82
theorem :: CARD_3:83
theorem Th84: :: CARD_3:84
theorem :: CARD_3:85
theorem Th86: :: CARD_3:86
theorem :: CARD_3:87
:: deftheorem Def10 defines with_common_domain CARD_3:def 10 :
theorem :: CARD_3:88
:: deftheorem CARD_3:def 11 :
canceled;
:: deftheorem Def12 defines DOM CARD_3:def 12 :
theorem :: CARD_3:89
:: deftheorem Def13 defines product" CARD_3:def 13 :
theorem :: CARD_3:90
theorem :: CARD_3:91
:: deftheorem Def14 defines product-like CARD_3:def 14 :
theorem Th92: :: CARD_3:92
theorem :: CARD_3:93
theorem Th94: :: CARD_3:94
theorem :: CARD_3:95
theorem :: CARD_3:96
theorem :: CARD_3:97
theorem Th98: :: CARD_3:98
theorem :: CARD_3:99
theorem :: CARD_3:100
theorem :: CARD_3:101
theorem Th8: :: CARD_3:102
theorem Th13: :: CARD_3:103
theorem :: CARD_3:104
theorem Th20: :: CARD_3:105
theorem :: CARD_3:106
theorem Th22: :: CARD_3:107
theorem :: CARD_3:108
Lm1:
( 0 = card 0 & 1 = card 1 & 2 = card 2 )
by CARD_1:def 5;
theorem :: CARD_3:109
theorem :: CARD_3:110
theorem Th26: :: CARD_3:111
theorem Th27: :: CARD_3:112
theorem Th28: :: CARD_3:113
theorem Th29: :: CARD_3:114
theorem Th30: :: CARD_3:115
Lm2:
omega is limit_ordinal
by ORDINAL1:def 12;
theorem Th31: :: CARD_3:116
theorem Th33: :: CARD_3:117
theorem Th34: :: CARD_3:118
theorem :: CARD_3:119
theorem :: CARD_3:120
theorem :: CARD_3:121
theorem :: CARD_3:122
theorem :: CARD_3:123
theorem :: CARD_3:124
theorem Th41: :: CARD_3:125
theorem :: CARD_3:126
:: deftheorem Def1 defines countable CARD_3:def 15 :
:: deftheorem defines denumerable CARD_3:def 16 :
theorem Th45: :: CARD_3:127
Th46:
for Y, X being set st Y c= X & X is countable holds
Y is countable
;
theorem Th47: :: CARD_3:128
theorem :: CARD_3:129
theorem :: CARD_3:130
theorem :: CARD_3:131
theorem Th59: :: CARD_3:132
theorem :: CARD_3:133
theorem Th63: :: CARD_3:134
theorem :: CARD_3:135
theorem Th68: :: CARD_3:136
theorem :: CARD_3:137
theorem Th70: :: CARD_3:138
for
K,
L,
M,
N being
Cardinal holds
( ( not (
K in L &
M in N ) & not (
K c= L &
M in N ) & not (
K in L &
M c= N ) & not (
K c= L &
M c= N ) ) or
K = 0 or
exp K,
M c= exp L,
N )
theorem :: CARD_3:139
theorem Th72: :: CARD_3:140
theorem :: CARD_3:141
theorem Th74: :: CARD_3:142
theorem :: CARD_3:143
theorem :: CARD_3:144
theorem :: CARD_3:145
theorem :: CARD_3:146