HALLMAR1: The {H}all {M}arriage {T}heorem

:: The {H}all {M}arriage {T}heorem
:: by Ewa Romanowicz and Adam Grabowski
::
:: Received May 11, 2004
:: Copyright (c) 2004-2011 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)

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 non empty Relation-like non-empty NAT -defined bool F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool F;
existence

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

proof end;

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 & j in dom A & x in A . j ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines union HALLMAR1:def 1 :

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 by Th3, FINSET_1:13;

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)

proof end;

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;

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 & ( 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Cut HALLMAR1:def 2 :

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;

begin

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 :Def3: :: 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 Def3 defines is_a_system_of_different_representatives_of HALLMAR1:def 3 :

definition

let F be finite set ;
let A be FinSequence of bool F;
attr A 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 :

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 FinSequence of bool F;
existence

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 FinSequence of bool F;
existence

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 FinSequence of bool F;
coherence 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;

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 & ( for j being Element of NAT st j in dom A & j <> i holds
A . j = it . j ) & it . i c= A . i );
existence

proof end;

end;

:: deftheorem Def5 defines Reduction HALLMAR1:def 5 :

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

proof end;

end;

:: deftheorem Def6 defines Reduction HALLMAR1:def 6 :

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

proof end;

end;

:: deftheorem Def7 defines Singlification HALLMAR1:def 7 :

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

proof end;

end;

:: deftheorem Def8 defines Singlification HALLMAR1:def 8 :

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 Singlification of A,k;
coherence

proof end;

end;

registration

let F be non empty finite set ;
let A be non empty FinSequence of bool F;
cluster -> non empty Singlification of A;
coherence

proof end;

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

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;

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;