:: by Ewa Romanowicz and Adam Grabowski

::

:: Received May 11, 2004

:: Copyright (c) 2004-2021 Association of Mizar Users

registration

let F be non empty set ;

ex b_{1} being FinSequence of bool F st

( not b_{1} is empty & b_{1} is non-empty )

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

( not b

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

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 ;

coherence

A . i is finite

end;
let A be FinSequence of bool F;

let i be Element of NAT ;

coherence

A . i is finite

proof end;

definition

let F be set ;

let A be FinSequence of bool F;

let J be set ;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff ex j being set st

( j in J & j in dom A & x in A . j ) )

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} 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_{2} iff ex j being set st

( j in J & j in dom A & x in A . j ) ) ) holds

b_{1} = b_{2}

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

ex b

for x being object holds

( x in b

( j in J & j in dom A & x in A . j ) )

proof end;

uniqueness for b

( x in b

( j in J & j in dom A & x in A . j ) ) ) & ( for x being object holds

( x in b

( j in J & j in dom A & x in A . j ) ) ) holds

b

proof end;

:: deftheorem Def1 defines union HALLMAR1:def 1 :

for F being set

for A being FinSequence of bool F

for J, b_{4} being set holds

( b_{4} = union (A,J) iff for x being object holds

( x in b_{4} iff ex j being set st

( j in J & j in dom A & x in A . j ) ) );

for F being set

for A being FinSequence of bool F

for J, b

( b

( x in b

( j in J & j in dom A & x in A . j ) ) );

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)

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 ;

coherence

union (A,J) is finite by Th3, FINSET_1:1;

end;
let A be FinSequence of bool F;

let J be set ;

coherence

union (A,J) is finite by Th3, FINSET_1:1;

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

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)

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

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

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

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 ;

ex b_{1} being FinSequence of bool F st

( dom b_{1} = dom A & ( for k being Element of NAT st k in dom b_{1} holds

( ( i = k implies b_{1} . k = (A . k) \ {x} ) & ( i <> k implies b_{1} . k = A . k ) ) ) )

for b_{1}, b_{2} being FinSequence of bool F st dom b_{1} = dom A & ( for k being Element of NAT st k in dom b_{1} holds

( ( i = k implies b_{1} . k = (A . k) \ {x} ) & ( i <> k implies b_{1} . k = A . k ) ) ) & dom b_{2} = dom A & ( for k being Element of NAT st k in dom b_{2} holds

( ( i = k implies b_{2} . k = (A . k) \ {x} ) & ( i <> k implies b_{2} . k = A . k ) ) ) holds

b_{1} = b_{2}

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

ex b

( dom b

( ( i = k implies b

proof end;

uniqueness for b

( ( i = k implies b

( ( i = k implies b

b

proof 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_{5} being FinSequence of bool F holds

( b_{5} = Cut (A,i,x) iff ( dom b_{5} = dom A & ( for k being Element of NAT st k in dom b_{5} holds

( ( i = k implies b_{5} . k = (A . k) \ {x} ) & ( i <> k implies b_{5} . k = A . k ) ) ) ) );

for F being finite set

for A being FinSequence of bool F

for i being Element of NAT

for x being set

for b

( b

( ( i = k implies b

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

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

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)

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

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 ;

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

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

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

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

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

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 ;

ex b_{1} being FinSequence of bool F st

( b_{1} is Hall & not b_{1} is empty )

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

( b

proof end;

registration

let F be finite set ;

ex b_{1} being FinSequence of bool F st b_{1} is Hall

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

existence ex b

proof 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

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 ;

coherence

for b_{1} being non empty FinSequence of bool F st b_{1} is Hall holds

b_{1} is non-empty
by Th15;

end;
coherence

for b

b

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

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

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

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 ;

ex b_{1} being FinSequence of bool F st

( dom b_{1} = dom A & ( for j being Element of NAT st j in dom A & j <> i holds

A . j = b_{1} . j ) & b_{1} . i c= A . i )

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

ex b

( dom b

A . j = b

proof 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_{4} being FinSequence of bool F holds

( b_{4} is Reduction of A,i iff ( dom b_{4} = dom A & ( for j being Element of NAT st j in dom A & j <> i holds

A . j = b_{4} . j ) & b_{4} . i c= A . i ) );

for F being set

for A being FinSequence of bool F

for i being Element of NAT

for b

( b

A . j = b

definition

let F be set ;

let A be FinSequence of bool F;

ex b_{1} being FinSequence of bool F st

( dom b_{1} = dom A & ( for i being Element of NAT st i in dom A holds

b_{1} . i c= A . i ) )

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

it . i c= A . i ) );

ex b

( dom b

b

proof end;

:: deftheorem Def6 defines Reduction HALLMAR1:def 6 :

for F being set

for A, b_{3} being FinSequence of bool F holds

( b_{3} is Reduction of A iff ( dom b_{3} = dom A & ( for i being Element of NAT st i in dom A holds

b_{3} . i c= A . i ) ) );

for F being set

for A, b

( b

b

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

existence

ex b_{1} being Reduction of A st card (b_{1} . i) = 1

end;
let A be FinSequence of bool F;

let i be Nat;

assume that

A1: i in dom A and

A2: A . i <> {} ;

existence

ex b

proof 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_{4} being Reduction of A holds

( b_{4} is Singlification of A,i iff card (b_{4} . i) = 1 );

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

( b

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

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

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

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

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

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 )

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

for A being FinSequence of bool F

for i being Element of NAT holds A is Reduction of A,i

proof end;

definition

let F be non empty set ;

let A be FinSequence of bool F;

assume A1: A is non-empty ;

ex b_{1} being Reduction of A st

for i being Element of NAT st i in dom A holds

card (b_{1} . i) = 1

end;
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 for i being Element of NAT st i in dom A holds

card (it . i) = 1;

ex b

for i being Element of NAT st i in dom A holds

card (b

proof 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_{3} being Reduction of A holds

( b_{3} is Singlification of A iff for i being Element of NAT st i in dom A holds

card (b_{3} . i) = 1 );

for F being non empty set

for A being FinSequence of bool F st A is non-empty holds

for b

( b

card (b

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

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 ;

coherence

for b_{1} being Singlification of A,k holds not b_{1} is empty

end;
let A be non empty FinSequence of bool F;

let k be Element of NAT ;

coherence

for b

proof end;

registration

let F be non empty finite set ;

let A be non empty FinSequence of bool F;

coherence

for b_{1} being Singlification of A holds not b_{1} is empty

end;
let A be non empty FinSequence of bool F;

coherence

for b

proof 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

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 )

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

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

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 )

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;