:: The {H}all {M}arriage {T}heorem
:: by Ewa Romanowicz and Adam Grabowski
::
:: Received May 11, 2004
:: 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{ F₁() -> Element of NAT , P₁[ set ] } :

for k being Element of NAT st 1 <= k & k <= F₁() holds
P₁[k]

provided

A1: ( P₁[F₁()] & F₁() >= 2 ) and
A2: for k being Element of NAT st 1 <= k & k < F₁() & P₁[k + 1] holds
P₁[k]

proof end;

scheme :: HALLMAR1:sch 2
Regr2{ P₁[ set ] } :

P₁[1]

provided

A1: ex n being Element of NAT st
( n > 1 & P₁[n] ) and
A2: for k being Element of NAT st k >= 1 & P₁[k + 1] holds
P₁[k]

proof end;

registration

let F be non empty set ;

cluster Relation-like non-empty NAT -defined bool F -valued non empty Function-like finite FinSequence-like FinSubsequence-like for FinSequence of bool F;

existence
ex b₁ being FinSequence of bool F st
( not b₁ is empty & b₁ 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 b₁ being set st
for x being object holds
( x in b₁ iff ex j being set st
( j in J & j in dom A & x in A . j ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff ex j being set st
( j in J & j in dom A & x in A . j ) ) ) & ( for x being object holds
( x in b₂ iff ex j being set st
( j in J & j in dom A & x in A . j ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines union HALLMAR1:def 1 :
for F being set
for A being FinSequence of bool F
for J, b₄ being set holds
( b₄ = union (A,J) iff for x being object holds
( x in b₄ 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 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

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 b₁ being FinSequence of bool F st
( dom b₁ = dom A & ( for k being Element of NAT st k in dom b₁ holds
( ( i = k implies b₁ . k = (A . k) \ {x} ) & ( i <> k implies b₁ . k = A . k ) ) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of bool F st dom b₁ = dom A & ( for k being Element of NAT st k in dom b₁ holds
( ( i = k implies b₁ . k = (A . k) \ {x} ) & ( i <> k implies b₁ . k = A . k ) ) ) & dom b₂ = dom A & ( for k being Element of NAT st k in dom b₂ holds
( ( i = k implies b₂ . k = (A . k) \ {x} ) & ( i <> k implies b₂ . k = A . k ) ) ) holds
b₁ = b₂

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 b₅ being FinSequence of bool F holds
( b₅ = Cut (A,i,x) iff ( dom b₅ = dom A & ( for k being Element of NAT st k in dom b₅ holds
( ( i = k implies b₅ . k = (A . k) \ {x} ) & ( i <> k implies b₅ . 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 ;

cluster Relation-like NAT -defined bool F -valued non empty Function-like finite FinSequence-like FinSubsequence-like Hall for FinSequence of bool F;

existence
ex b₁ being FinSequence of bool F st
( b₁ is Hall & not b₁ is empty )

proof end;

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 b₁ being FinSequence of bool F st b₁ 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 b₁ being non empty FinSequence of bool F st b₁ is Hall holds
b₁ 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 b₁ being FinSequence of bool F st
( dom b₁ = dom A & ( for j being Element of NAT st j in dom A & j <> i holds
A . j = b₁ . j ) & b₁ . 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 b₄ being FinSequence of bool F holds
( b₄ is Reduction of A,i iff ( dom b₄ = dom A & ( for j being Element of NAT st j in dom A & j <> i holds
A . j = b₄ . j ) & b₄ . 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 b₁ being FinSequence of bool F st
( dom b₁ = dom A & ( for i being Element of NAT st i in dom A holds
b₁ . i c= A . i ) )

proof end;

end;

:: deftheorem Def6 defines Reduction HALLMAR1:def 6 :
for F being set
for A, b₃ being FinSequence of bool F holds
( b₃ is Reduction of A iff ( dom b₃ = dom A & ( for i being Element of NAT st i in dom A holds
b₃ . 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 b₁ being Reduction of A st card (b₁ . 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 b₄ being Reduction of A holds
( b₄ is Singlification of A,i iff card (b₄ . 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 b₁ being Reduction of A st
for i being Element of NAT st i in dom A holds
card (b₁ . 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 b₃ being Reduction of A holds
( b₃ is Singlification of A iff for i being Element of NAT st i in dom A holds
card (b₃ . 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 b₁ being Singlification of A,k holds not b₁ 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 b₁ being Singlification of A holds not b₁ 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;