:: The {H}all {M}arriage {T}heorem
:: by Ewa Romanowicz and Adam Grabowski
::
:: Received May 11, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

theorem Th1: :: HALLMAR1:1
for X, Y being finite set holds (card (X \/ Y)) + (card (X /\ Y)) = (card X) + (card Y)
proofend;

scheme :: HALLMAR1:sch 1
Regr11{ F1() ->  Element of NAT , P1[ set ] } :
 for k being Element of NAT st 1 <= k &amp; k <= F1() holds
P1[k]
provided
A1: ( P1[F1()] &amp; F1() >= 2 ) and
A2: for k being Element of NAT st 1 <= k &amp; k < F1() &amp; P1[k + 1] holds
P1[k]
proofend;

scheme :: HALLMAR1:sch 2
Regr2{ P1[ set ] } :
 P1[1]
provided
A1: ex n being Element of NAT st
( n > 1 &amp; P1[n] ) and
A2: for k being Element of NAT st k >= 1 &amp; P1[k + 1] holds
P1[k]
proofend;

registration
let F be non empty set ;
cluster non empty Relation-like non-empty NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like for FinSequence of bool F;
existence
 ex b1 being FinSequence of bool F st
( not b1 is empty &amp; b1 is non-empty )
proofend;
end;

theorem Th2: :: HALLMAR1:2
for F being non empty set
for f being non-empty FinSequence of bool F
for i being Element of NAT st i in dom f holds
f . i <> {}
proofend;

registration
let F be finite set ;
let A be FinSequence of bool F;
let i be Element of NAT ;
clusterA . i ->  finite ;
coherence
 A . i is finite
proofend;
end;

begin

definition
let F be set ;
let A be FinSequence of bool F;
let J be set ;
func union (A,J) ->  set  means :Def1: :: HALLMAR1:def 1
 for x being set holds
( x in it iff ex j being set st
( j in J &amp; j in dom A &amp; x in A . j ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex j being set st
( j in J &amp; j in dom A &amp; x in A . j ) )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex j being set st
( j in J &amp; j in dom A &amp; x in A . j ) ) ) &amp; ( for x being set holds
( x in b2 iff ex j being set st
( j in J &amp; j in dom A &amp; x in A . j ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines union HALLMAR1:def_1_:_
 for F being set
for A being FinSequence of bool F
for J, b4 being set holds
( b4 = union (A,J) iff for x being set holds
( x in b4 iff ex j being set st
( j in J &amp; j in dom A &amp; x in A . j ) ) );

theorem Th3: :: HALLMAR1:3
for F being set
for A being FinSequence of bool F
for J being set holds union (A,J) c= F
proofend;

theorem :: HALLMAR1:4
for F being finite set
for A being FinSequence of bool F
for J, K being set st J c= K holds
union (A,J) c= union (A,K)
proofend;

registration
let F be finite set ;
let A be FinSequence of bool F;
let J be set ;
cluster union (A,J) ->  finite ;
coherence
 union (A,J) is finite by Th3, FINSET_1:1;
end;

theorem Th5: :: HALLMAR1:5
for F being finite set
for A being FinSequence of bool F
for i being Element of NAT st i in dom A holds
union (A,{i}) = A . i
proofend;

theorem Th6: :: HALLMAR1:6
for F being finite set
for A being FinSequence of bool F
for i, j being Element of NAT st i in dom A &amp; j in dom A holds
union (A,{i,j}) = (A . i) \/ (A . j)
proofend;

theorem Th7: :: HALLMAR1:7
for J being set
for F being finite set
for A being FinSequence of bool F
for i being Element of NAT st i in J &amp; i in dom A holds
A . i c= union (A,J)
proofend;

theorem Th8: :: HALLMAR1:8
for J being set
for F being finite set
for i being Element of NAT
for A being FinSequence of bool F st i in J &amp; i in dom A holds
union (A,J) = (union (A,(J \ {i}))) \/ (A . i)
proofend;

theorem Th9: :: HALLMAR1:9
for J1, J2 being set
for F being finite set
for i being Element of NAT
for A being FinSequence of bool F st i in dom A holds
union (A,(({i} \/ J1) \/ J2)) = (A . i) \/ (union (A,(J1 \/ J2)))
proofend;

theorem Th10: :: HALLMAR1:10
for F being finite set
for A being FinSequence of bool F
for i being Element of NAT
for x, y being set st x <> y &amp; x in A . i &amp; y in A . i holds
((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i
proofend;

begin

definition
let F be finite set ;
let A be FinSequence of bool F;
let i be Element of NAT ;
let x be set ;
func Cut (A,i,x) ->  FinSequence of bool F means :Def2: :: HALLMAR1:def 2
( dom it = dom A &amp; ( for k being Element of NAT st k in dom it holds
( ( i = k implies it . k = (A . k) \ {x} ) &amp; ( i <> k implies it . k = A . k ) ) ) );
existence
 ex b1 being FinSequence of bool F st
( dom b1 = dom A &amp; ( for k being Element of NAT st k in dom b1 holds
( ( i = k implies b1 . k = (A . k) \ {x} ) &amp; ( i <> k implies b1 . k = A . k ) ) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of bool F st dom b1 = dom A &amp; ( for k being Element of NAT st k in dom b1 holds
( ( i = k implies b1 . k = (A . k) \ {x} ) &amp; ( i <> k implies b1 . k = A . k ) ) ) &amp; dom b2 = dom A &amp; ( for k being Element of NAT st k in dom b2 holds
( ( i = k implies b2 . k = (A . k) \ {x} ) &amp; ( i <> k implies b2 . k = A . k ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines Cut HALLMAR1:def_2_:_
 for F being finite set
for A being FinSequence of bool F
for i being Element of NAT
for x being set
for b5 being FinSequence of bool F holds
( b5 = Cut (A,i,x) iff ( dom b5 = dom A &amp; ( for k being Element of NAT st k in dom b5 holds
( ( i = k implies b5 . k = (A . k) \ {x} ) &amp; ( i <> k implies b5 . k = A . k ) ) ) ) );

theorem Th11: :: HALLMAR1:11
for F being finite set
for A being FinSequence of bool F
for i being Element of NAT
for x being set st i in dom A &amp; x in A . i holds
card ((Cut (A,i,x)) . i) = (card (A . i)) - 1
proofend;

theorem Th12: :: HALLMAR1:12
for F being finite set
for A being FinSequence of bool F
for i being Element of NAT
for x, J being set holds union ((Cut (A,i,x)),(J \ {i})) = union (A,(J \ {i}))
proofend;

theorem Th13: :: HALLMAR1:13
for F being finite set
for A being FinSequence of bool F
for i being Element of NAT
for x, J being set st not i in J holds
union (A,J) = union ((Cut (A,i,x)),J)
proofend;

theorem Th14: :: HALLMAR1:14
for F being finite set
for A being FinSequence of bool F
for i being Element of NAT
for x, J being set st i in dom (Cut (A,i,x)) &amp; i in J holds
union ((Cut (A,i,x)),J) = (union (A,(J \ {i}))) \/ ((A . i) \ {x})
proofend;

begin

definition
let F be finite set ;
let X be FinSequence of bool F;
let A be set ;
predA is_a_system_of_different_representatives_of X means :Def3: :: HALLMAR1:def 3
 ex f being FinSequence of F st
( f = A &amp; dom X = dom f &amp; ( for i being Element of NAT st i in dom f holds
f . i in X . i ) &amp; f is one-to-one );
end;

:: deftheorem Def3 defines is_a_system_of_different_representatives_of HALLMAR1:def_3_:_
 for F being finite set
for X being FinSequence of bool F
for A being set holds
( A is_a_system_of_different_representatives_of X iff ex f being FinSequence of F st
( f = A &amp; dom X = dom f &amp; ( for i being Element of NAT st i in dom f holds
f . i in X . i ) &amp; f is one-to-one ) );

definition
let F be finite set ;
let A be FinSequence of bool F;
attrA is Hall  means :Def4: :: HALLMAR1:def 4
 for J being finite set st J c= dom A holds
card J <= card (union (A,J));
end;

:: deftheorem Def4 defines Hall HALLMAR1:def_4_:_
 for F being finite set
for A being FinSequence of bool F holds
( A is Hall iff for J being finite set st J c= dom A holds
card J <= card (union (A,J)) );

registration
let F be non empty finite set ;
cluster non empty Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like Hall for FinSequence of bool F;
existence
 ex b1 being FinSequence of bool F st
( b1 is Hall &amp; not b1 is empty )
proofend;
end;

registration
let F be finite set ;
cluster Relation-like NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like Hall for FinSequence of bool F;
existence
 ex b1 being FinSequence of bool F st b1 is Hall
proofend;
end;

theorem Th15: :: HALLMAR1:15
for F being finite set
for A being non empty FinSequence of bool F st A is Hall holds
A is non-empty
proofend;

registration
let F be finite set ;
cluster non empty Hall  ->  non empty non-empty for FinSequence of bool F;
coherence
 for b1 being non empty FinSequence of bool F st b1 is Hall holds
b1 is non-empty by Th15;
end;

theorem Th16: :: HALLMAR1:16
for F being finite set
for A being FinSequence of bool F
for i being Element of NAT st i in dom A &amp; A is Hall holds
card (A . i) >= 1
proofend;

theorem Th17: :: HALLMAR1:17
for F being non empty finite set
for A being non empty FinSequence of bool F st ( for i being Element of NAT st i in dom A holds
card (A . i) = 1 ) &amp; A is Hall holds
ex X being set st X is_a_system_of_different_representatives_of A
proofend;

theorem Th18: :: HALLMAR1:18
for F being finite set
for A being FinSequence of bool F st ex X being set st X is_a_system_of_different_representatives_of A holds
A is Hall
proofend;

begin

definition
let F be set ;
let A be FinSequence of bool F;
let i be Element of NAT ;
mode Reduction of A,i ->  FinSequence of bool F means :Def5: :: HALLMAR1:def 5
( dom it = dom A &amp; ( for j being Element of NAT st j in dom A &amp; j <> i holds
A . j = it . j ) &amp; it . i c= A . i );
existence
 ex b1 being FinSequence of bool F st
( dom b1 = dom A &amp; ( for j being Element of NAT st j in dom A &amp; j <> i holds
A . j = b1 . j ) &amp; b1 . i c= A . i )
proofend;
end;

:: deftheorem Def5 defines Reduction HALLMAR1:def_5_:_
 for F being set
for A being FinSequence of bool F
for i being Element of NAT
for b4 being FinSequence of bool F holds
( b4 is Reduction of A,i iff ( dom b4 = dom A &amp; ( for j being Element of NAT st j in dom A &amp; j <> i holds
A . j = b4 . j ) &amp; b4 . i c= A . i ) );

definition
let F be set ;
let A be FinSequence of bool F;
mode Reduction of A ->  FinSequence of bool F means :Def6: :: HALLMAR1:def 6
( dom it = dom A &amp; ( for i being Element of NAT st i in dom A holds
it . i c= A . i ) );
existence
 ex b1 being FinSequence of bool F st
( dom b1 = dom A &amp; ( for i being Element of NAT st i in dom A holds
b1 . i c= A . i ) )
proofend;
end;

:: deftheorem Def6 defines Reduction HALLMAR1:def_6_:_
 for F being set
for A, b3 being FinSequence of bool F holds
( b3 is Reduction of A iff ( dom b3 = dom A &amp; ( for i being Element of NAT st i in dom A holds
b3 . i c= A . i ) ) );

definition
let F be set ;
let A be FinSequence of bool F;
let i be Element of NAT ;
assume that
A1: i in dom A and
A2: A . i <> {} ;
mode Singlification of A,i ->  Reduction of A means :Def7: :: HALLMAR1:def 7
 card (it . i) = 1;
existence
 ex b1 being Reduction of A st card (b1 . i) = 1
proofend;
end;

:: deftheorem Def7 defines Singlification HALLMAR1:def_7_:_
 for F being set
for A being FinSequence of bool F
for i being Element of NAT st i in dom A &amp; A . i <> {} holds
for b4 being Reduction of A holds
( b4 is Singlification of A,i iff card (b4 . i) = 1 );

theorem Th19: :: HALLMAR1:19
for F being finite set
for A being FinSequence of bool F
for i being Element of NAT
for C being Reduction of A,i holds C is Reduction of A
proofend;

theorem Th20: :: HALLMAR1:20
for F being finite set
for A being FinSequence of bool F
for i being Element of NAT
for x being set st i in dom A holds
Cut (A,i,x) is Reduction of A,i
proofend;

theorem Th21: :: HALLMAR1:21
for F being finite set
for A being FinSequence of bool F
for i being Element of NAT
for x being set st i in dom A holds
Cut (A,i,x) is Reduction of A
proofend;

theorem Th22: :: HALLMAR1:22
for F being finite set
for A being FinSequence of bool F
for B being Reduction of A
for C being Reduction of B holds C is Reduction of A
proofend;

theorem :: HALLMAR1:23
for F being non empty finite set
for A being non-empty FinSequence of bool F
for i being Element of NAT
for B being Singlification of A,i st i in dom A holds
B . i <> {}
proofend;

theorem Th24: :: HALLMAR1:24
for F being non empty finite set
for A being non-empty FinSequence of bool F
for i, j being Element of NAT
for B being Singlification of A,i
for C being Singlification of B,j st i in dom A &amp; j in dom A &amp; C . i <> {} &amp; B . j <> {} holds
( C is Singlification of A,j &amp; C is Singlification of A,i )
proofend;

theorem :: HALLMAR1:25
for F being set
for A being FinSequence of bool F
for i being Element of NAT holds A is Reduction of A,i
proofend;

theorem Th26: :: HALLMAR1:26
for F being set
for A being FinSequence of bool F holds A is Reduction of A
proofend;

definition
let F be non empty set ;
let A be FinSequence of bool F;
assume A1: A is non-empty ;
mode Singlification of A ->  Reduction of A means :Def8: :: HALLMAR1:def 8
 for i being Element of NAT st i in dom A holds
card (it . i) = 1;
existence
 ex b1 being Reduction of A st
for i being Element of NAT st i in dom A holds
card (b1 . i) = 1
proofend;
end;

:: deftheorem Def8 defines Singlification HALLMAR1:def_8_:_
 for F being non empty set
for A being FinSequence of bool F st A is non-empty holds
for b3 being Reduction of A holds
( b3 is Singlification of A iff for i being Element of NAT st i in dom A holds
card (b3 . i) = 1 );

theorem Th27: :: HALLMAR1:27
for F being non empty finite set
for A being non empty non-empty FinSequence of bool F
for f being Function holds
( f is Singlification of A iff ( dom f = dom A &amp; ( for i being Element of NAT st i in dom A holds
f is Singlification of A,i ) ) )
proofend;

registration
let F be non empty finite set ;
let A be non empty FinSequence of bool F;
let k be Element of NAT ;
cluster  ->  non empty for Singlification of A,k;
coherence
 for b1 being Singlification of A,k holds not b1 is empty
proofend;
end;

registration
let F be non empty finite set ;
let A be non empty FinSequence of bool F;
cluster  ->  non empty for Singlification of A;
coherence
 for b1 being Singlification of A holds not b1 is empty
proofend;
end;

begin

theorem Th28: :: HALLMAR1:28
for F being non empty finite set
for A being non empty FinSequence of bool F
for X being set
for B being Reduction of A st X is_a_system_of_different_representatives_of B holds
X is_a_system_of_different_representatives_of A
proofend;

theorem Th29: :: HALLMAR1:29
for F being finite set
for A being FinSequence of bool F st A is Hall holds
for i being Element of NAT st card (A . i) >= 2 holds
ex x being set st
( x in A . i &amp; Cut (A,i,x) is Hall )
proofend;

theorem Th30: :: HALLMAR1:30
for F being finite set
for A being FinSequence of bool F
for i being Element of NAT st i in dom A &amp; A is Hall holds
ex G being Singlification of A,i st G is Hall
proofend;

theorem Th31: :: HALLMAR1:31
for F being non empty finite set
for A being non empty FinSequence of bool F st A is Hall holds
ex G being Singlification of A st G is Hall
proofend;

:: [WP: ] Hall_Marriage_Theorem
theorem :: HALLMAR1:32
for F being non empty finite set
for A being non empty FinSequence of bool F holds
( ex X being set st X is_a_system_of_different_representatives_of A iff A is Hall )
proofend;