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

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

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

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

registration
let F be non empty set ;
existence
ex b1 being FinSequence of bool F st
( not b1 is empty & b1 is non-empty )
proof end;
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 <> {}
proof end;

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

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 object holds
( x in it iff ex j being set st
( j in J & j in dom A & x in A . j ) );
existence
ex b1 being set st
for x being object holds
( x in b1 iff ex j being set st
( j in J & j in dom A & x in A . j ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being object holds
( x in b1 iff ex j being set st
( j in J & j in dom A & x in A . j ) ) ) & ( for x being object holds
( x in b2 iff ex j being set st
( j in J & j in dom A & x in A . j ) ) ) holds
b1 = b2
proof end;
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 object holds
( x in b4 iff ex j being set st
( j in J & j in dom A & 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
proof end;

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)
proof end;

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 ;
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
proof end;

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 & j in dom A holds
union (A,{i,j}) = (A . i) \/ (A . j)
proof end;

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 & i in dom A holds
A . i c= union (A,J) by Def1;

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 & i in dom A holds
union (A,J) = (union (A,(J \ {i}))) \/ (A . i)
proof end;

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)))
proof end;

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 & x in A . i & y in A . i holds
((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i
proof end;

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 & ( for k being Element of NAT st k in dom it holds
( ( i = k implies it . k = (A . k) \ {x} ) & ( i <> k implies it . k = A . k ) ) ) );
existence
ex b1 being FinSequence of bool F st
( dom b1 = dom A & ( for k being Element of NAT st k in dom b1 holds
( ( i = k implies b1 . k = (A . k) \ {x} ) & ( i <> k implies b1 . k = A . k ) ) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of bool F st dom b1 = dom A & ( for k being Element of NAT st k in dom b1 holds
( ( i = k implies b1 . k = (A . k) \ {x} ) & ( i <> k implies b1 . k = A . k ) ) ) & dom b2 = dom A & ( for k being Element of NAT st k in dom b2 holds
( ( i = k implies b2 . k = (A . k) \ {x} ) & ( i <> k implies b2 . k = A . k ) ) ) holds
b1 = b2
proof end;
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 & ( for k being Element of NAT st k in dom b5 holds
( ( i = k implies b5 . k = (A . k) \ {x} ) & ( 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 & x in A . i holds
card ((Cut (A,i,x)) . i) = (card (A . i)) - 1
proof end;

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}))
proof end;

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)
proof end;

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)) & i in J holds
union ((Cut (A,i,x)),J) = (union (A,(J \ {i}))) \/ ((A . i) \ {x})
proof end;

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

:: deftheorem 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 & dom X = dom f & ( for i being Element of NAT st i in dom f holds
f . i in X . i ) & f is one-to-one ) );

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

:: deftheorem 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 ;
existence
ex b1 being FinSequence of bool F st
( b1 is Hall & not b1 is empty )
proof end;
end;

registration
let F be finite set ;
existence
ex b1 being FinSequence of bool F st b1 is Hall
proof end;
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
proof end;

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 & A is Hall holds
card (A . i) >= 1
proof end;

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 ) & A is Hall holds
ex X being set st X is_a_system_of_different_representatives_of A
proof end;

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
proof end;

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 & ( for j being Element of NAT st j in dom A & j <> i holds
A . j = it . j ) & it . i c= A . i );
existence
ex b1 being FinSequence of bool F st
( dom b1 = dom A & ( for j being Element of NAT st j in dom A & j <> i holds
A . j = b1 . j ) & b1 . i c= A . i )
proof end;
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 & ( for j being Element of NAT st j in dom A & j <> i holds
A . j = b4 . j ) & 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 & ( 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 & ( for i being Element of NAT st i in dom A holds
b1 . i c= A . i ) )
proof end;
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 & ( 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 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
proof end;
end;

:: deftheorem Def7 defines Singlification HALLMAR1:def 7 :
for F being set
for A being FinSequence of bool F
for i being Nat st i in dom A & 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
proof end;

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
proof end;

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
proof end;

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
proof end;

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 <> {}
proof end;

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 & j in dom A & C . i <> {} & B . j <> {} holds
( C is Singlification of A,j & C is Singlification of A,i )
proof end;

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
proof end;

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

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
proof end;
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 & ( for i being Element of NAT st i in dom A holds
f is Singlification of A,i ) ) )
proof end;

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
proof end;
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
proof end;
end;

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
proof end;

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 & Cut (A,i,x) is Hall )
proof end;

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 & A is Hall holds
ex G being Singlification of A,i st G is Hall
proof end;

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
proof end;

:: 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 )
proof end;