CARD_3: K\"onig's Theorem

correctness ;
defpred S₁[ object ] means ex g being Function st
( $1 = g & dom g = dom f & ( for x being object st x in dom f holds
g . x in f . x ) );

func product f -> set means :Def5: :: CARD_3:def 5
for x being object holds
( x in it iff ex g being Function st
( x = g & dom g = dom f & ( for y being object st y in dom f holds
g . y in f . y ) ) );

existence

proof end;

uniqueness

proof end;

end;

:: 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 Th1: :: CARD_3:1

for ff being Cardinal-Function holds Card ff = ff

proof end;

theorem :: CARD_3:2

for X, Y being set holds Card (X --> Y) = X --> (card Y)

proof end;

theorem :: CARD_3:3

disjoin {} = {} by Def3, RELAT_1:38;

theorem Th4: :: CARD_3:4

for x being object
for X being set holds disjoin (x .--> X) = x .--> [:X,{x}:]

proof end;

theorem :: CARD_3:5

for x, y being object
for f being Function st x in dom f & y in dom f & x <> y holds
(disjoin f) . x misses (disjoin f) . y

proof end;

theorem Th6: :: CARD_3:6

for X, Y being set holds Union (X --> Y) c= Y

proof end;

theorem Th7: :: CARD_3:7

for X, Y being set st X <> {} holds
Union (X --> Y) = Y

proof end;

theorem :: CARD_3:8

for x being object
for Y being set holds Union (x .--> Y) = Y by Th7;

theorem Th9: :: CARD_3:9

for f, g being Function holds
( g in product f iff ( dom g = dom f & ( for x being object st x in dom f holds
g . x in f . x ) ) )

proof end;

theorem Th10: :: CARD_3:10

product {} = {{}}

proof end;

theorem Th11: :: CARD_3:11

for X, Y being set holds Funcs (X,Y) = product (X --> Y)

proof end;

defpred S₁[ object ] means $1 is Function;

definition

let x be object ;
let X be set ;
defpred S₂[ object , object ] means ex g being Function st
( $1 = g & $2 = g . x );

func pi (X,x) -> set means :Def6: :: CARD_3:def 6
for y being object holds
( y in it iff ex f being Function st
( f in X & y = f . x ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines pi CARD_3:def 6 :

theorem :: CARD_3:12

for x being object
for f being Function st x in dom f & product f <> {} holds
pi ((product f),x) = f . x

proof end;

theorem :: CARD_3:13

for x being object holds pi ({},x) = {}

proof end;

theorem :: CARD_3:14

for x being object
for g being Function holds pi ({g},x) = {(g . x)}

proof end;

theorem :: CARD_3:15

for x being object
for f, g being Function holds pi ({f,g},x) = {(f . x),(g . x)}

proof end;

theorem Th16: :: CARD_3:16

for x being object
for X, Y being set holds pi ((X \/ Y),x) = (pi (X,x)) \/ (pi (Y,x))

proof end;

theorem :: CARD_3:17

for x being object
for X, Y being set holds pi ((X /\ Y),x) c= (pi (X,x)) /\ (pi (Y,x))

proof end;

theorem Th18: :: CARD_3:18

for x being object
for X, Y being set holds (pi (X,x)) \ (pi (Y,x)) c= pi ((X \ Y),x)

proof end;

theorem :: CARD_3:19

for x being object
for X, Y being set holds (pi (X,x)) \+\ (pi (Y,x)) c= pi ((X \+\ Y),x)

proof end;

theorem Th20: :: CARD_3:20

for x being object
for X being set holds card (pi (X,x)) c= card X

proof end;

theorem Th21: :: CARD_3:21

for x being object
for f being Function st x in Union (disjoin f) holds
ex y, z being object st x = [y,z]

proof end;

theorem Th22: :: CARD_3:22

for x being object
for f being Function holds
( x in Union (disjoin f) iff ( x `2 in dom f & x `1 in f . (x `2) & x = [(x `1),(x `2)] ) )

proof end;

theorem Th23: :: CARD_3:23

for f, g being Function st f c= g holds
disjoin f c= disjoin g

proof end;

theorem Th24: :: CARD_3:24

for f, g being Function st f c= g holds
Union f c= Union g

proof end;

theorem :: CARD_3:25

for X, Y being set holds Union (disjoin (Y --> X)) = [:X,Y:]

proof end;

theorem Th26: :: CARD_3:26

for f being Function holds
( product f = {} iff {} in rng f )

proof end;

theorem Th27: :: CARD_3:27

for f, g being Function st dom f = dom g & ( for x being object st x in dom f holds
f . x c= g . x ) holds
product f c= product g

proof end;

theorem :: CARD_3:28

for F being Cardinal-Function
for x being object st x in dom F holds
card (F . x) = F . x

proof end;

theorem Th29: :: CARD_3:29

for F being Cardinal-Function
for x being object st x in dom F holds
card ((disjoin F) . x) = F . x

proof end;

definition

let F be Cardinal-Function;

func Sum F -> Cardinal equals :: CARD_3:def 7
card (Union (disjoin F));

correctness ;

func Product F -> Cardinal equals :: CARD_3:def 8
card (product F);

correctness ;

end;

:: deftheorem defines Sum CARD_3:def 7 :

:: deftheorem defines Product CARD_3:def 8 :

theorem :: CARD_3:30

for F, G being Cardinal-Function st dom F = dom G & ( for x being object st x in dom F holds
F . x c= G . x ) holds
Sum F c= Sum G

proof end;

theorem :: CARD_3:31

for F being Cardinal-Function holds
( {} in rng F iff Product F = 0 )

proof end;

theorem :: CARD_3:32

for F, G being Cardinal-Function st dom F = dom G & ( for x being object st x in dom F holds
F . x c= G . x ) holds
Product F c= Product G by Th27, CARD_1:11;

theorem :: CARD_3:33

for F, G being Cardinal-Function st F c= G holds
Sum F c= Sum G

proof end;

theorem :: CARD_3:34

for F, G being Cardinal-Function st F c= G & not 0 in rng G holds
Product F c= Product G

proof end;

theorem :: CARD_3:35

for K being Cardinal holds Sum ({} --> K) = 0

proof end;

theorem :: CARD_3:36

for K being Cardinal holds Product ({} --> K) = 1 by Th10, CARD_1:30;

theorem :: CARD_3:37

for K being Cardinal
for x being object holds Sum (x .--> K) = K

proof end;

theorem :: CARD_3:38

for K being Cardinal
for x being object holds Product (x .--> K) = K

proof end;

theorem Th39: :: CARD_3:39

for f being Function holds card (Union f) c= Sum (Card f)

proof end;

theorem :: CARD_3:40

for F being Cardinal-Function holds card (Union F) c= Sum F

proof end;

Koenig Theorem

theorem :: CARD_3:41

for F, G being Cardinal-Function st dom F = dom G & ( for x being object st x in dom F holds
F . x in G . x ) holds
Sum F in Product G

proof end;

scheme :: CARD_3:sch 2
FuncSeparation{ F₁() -> set , F₂( object ) -> set , P₁[ object , object ] } :

ex f being Function st
( dom f = F₁() & ( for x being object st x in F₁() holds
for y being object holds
( y in f . x iff ( y in F₂(x) & P₁[x,y] ) ) ) )

proof end;

Lm1: for x being object
for R being Relation st x in field R holds
ex y being object st
( [x,y] in R or [y,x] in R )

proof end;

theorem Th42: :: CARD_3:42

for X being set st X is finite holds
card X in card omega

proof end;

theorem Th43: :: CARD_3:43

for A, B being Ordinal st card A in card B holds
A in B

proof end;

theorem Th44: :: CARD_3:44

for A being Ordinal
for M being Cardinal st card A in M holds
A in M

proof end;

theorem Th45: :: CARD_3:45

for X being set st X is c=-linear holds
ex Y being set st
( Y c= X & union Y = union X & ( for Z being set st Z c= Y & Z <> {} holds
ex Z1 being set st
( Z1 in Z & ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) ) ) )

proof end;

theorem :: CARD_3:46

for M being Cardinal
for X being set st ( for Z being set st Z in X holds
card Z in M ) & X is c=-linear holds
card (union X) c= M

proof end;

:: from AMI_1

registration

let f be Function;

cluster product f -> functional ;

coherence

proof end;

end;

registration

let A be set ;
let B be with_non-empty_elements set ;

cluster Function-like quasi_total -> non-empty for Element of bool [:A,B:];

coherence

proof end;

end;

:: from PRVECT_1

registration

let f be non-empty Function;

cluster product f -> non empty ;

coherence

proof end;

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))}

proof end;

:: from AMI_1, 2006.03.14, A.T.

theorem :: CARD_3:48

for x being object
for f being Function st x in product f holds
x is Function ;

definition

let f be Function;

func sproduct f -> set means :Def9: :: CARD_3:def 9
for x being object holds
( x in it iff ex g being Function st
( x = g & dom g c= dom f & ( for x being object st x in dom g holds
g . x in f . x ) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines sproduct CARD_3:def 9 :

registration

let f be Function;

cluster sproduct f -> non empty functional ;

coherence

proof end;

end;

theorem Th49: :: CARD_3:49

for f, g being Function st g in sproduct f holds
( dom g c= dom f & ( for x being object st x in dom g holds
g . x in f . x ) )

proof end;

theorem Th50: :: CARD_3:50

for f being Function holds {} in sproduct f

proof end;

registration

let f be Function;

cluster empty Relation-like Function-like for Element of sproduct f;

existence

proof end;

end;

theorem Th51: :: CARD_3:51

for f being Function holds product f c= sproduct f

proof end;

theorem Th52: :: CARD_3:52

for x being object
for f being Function st x in sproduct f holds
x is PartFunc of (dom f),(union (rng f))

proof end;

theorem Th53: :: CARD_3:53

for f, g, h being Function st g in product f & h in sproduct f holds
g +* h in product f

proof end;

theorem :: CARD_3:54

for f, g being Function st product f <> {} holds
( g in sproduct f iff ex h being Function st
( h in product f & g c= h ) )

proof end;

theorem Th55: :: CARD_3:55

for f being Function holds sproduct f c= PFuncs ((dom f),(union (rng f)))

proof end;

theorem Th56: :: CARD_3:56

for f, g being Function st f c= g holds
sproduct f c= sproduct g

proof end;

theorem Th57: :: CARD_3:57

sproduct {} = {{}}

proof end;

theorem :: CARD_3:58

for A, B being set holds PFuncs (A,B) = sproduct (A --> B)

proof end;

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 <> {} } )

proof end;

theorem Th60: :: CARD_3:60

for x, y being object
for f being Function st x in dom f & y in f . x holds
x .--> y in sproduct f

proof end;

theorem :: CARD_3:61

for f being Function holds
( sproduct f = {{}} iff for x being object st x in dom f holds
f . x = {} )

proof end;

theorem Th62: :: CARD_3:62

for f being Function
for A being set st A c= sproduct f & ( for h1, h2 being Function st h1 in A & h2 in A holds
h1 tolerates h2 ) holds
union A in sproduct f

proof end;

theorem :: CARD_3:63