:: HALLMAR1 semantic presentation
begin
theorem Th1: :: HALLMAR1:1
for X, Y being finite set holds (card (X \/ Y)) + (card (X /\ Y)) = (card X) + (card Y)
proof
let X, Y be finite set ; ::_thesis: (card (X \/ Y)) + (card (X /\ Y)) = (card X) + (card Y)
card (X \/ Y) = ((card X) + (card Y)) - (card (X /\ Y)) by CARD_2:45;
hence (card (X \/ Y)) + (card (X /\ Y)) = (card X) + (card Y) ; ::_thesis: verum
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
defpred S1[ Nat] means ( 1 <= $1 & $1 <= F1() & P1[$1] );
assume ex k being Element of NAT st S1[k] ; ::_thesis: contradiction
then A3: ex k being Nat st S1[k] ;
A4: for l being Nat st S1[l] holds
l <= F1() ;
consider l being Nat such that
A5: S1[l] and
A6: for n being Nat st S1[n] holds
n <= l from NAT_1:sch_6(A4, A3);
A7: l + 1 >= 1 by NAT_1:12;
A8: l < F1() by A1, A5, XXREAL_0:1;
then A9: l + 1 <= F1() by NAT_1:13;
A10: now__::_thesis:_P1[l_+_1]
assume P1[l + 1] ; ::_thesis: contradiction
then l + 1 <= l by A6, A9, A7;
hence contradiction by XREAL_1:29; ::_thesis: verum
end;
l in NAT by ORDINAL1:def_12;
hence contradiction by A2, A5, A8, A10; ::_thesis: verum
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
consider n being Element of NAT such that
A3: n > 1 and
A4: P1[n] by A1;
n >= 1 + 1 by A3, NAT_1:13;
then A5: ( P1[n] & n >= 2 ) by A4;
A6: for k being Element of NAT st 1 <= k & k < n & P1[k + 1] holds
P1[k] by A2;
for k being Element of NAT st 1 <= k & k <= n holds
P1[k] from HALLMAR1:sch_1(A5, A6);
hence P1[1] by A3; ::_thesis: verum
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 for FinSequence of bool F;
existence
ex b1 being FinSequence of bool F st
( not b1 is empty & b1 is non-empty )
proof
set x = the non empty Subset of F;
take v = <* the non empty Subset of F*>; ::_thesis: ( not v is empty & v is non-empty )
thus not v is empty ; ::_thesis: v is non-empty
rng v = { the non empty Subset of F} by FINSEQ_1:39;
then not {} in rng v by TARSKI:def_1;
hence v is non-empty by RELAT_1:def_9; ::_thesis: verum
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
let F be non empty set ; ::_thesis: for f being non-empty FinSequence of bool F
for i being Element of NAT st i in dom f holds
f . i <> {}
let f be non-empty FinSequence of bool F; ::_thesis: for i being Element of NAT st i in dom f holds
f . i <> {}
let i be Element of NAT ; ::_thesis: ( i in dom f implies f . i <> {} )
assume A1: i in dom f ; ::_thesis: f . i <> {}
assume f . i = {} ; ::_thesis: contradiction
then {} in rng f by A1, FUNCT_1:3;
hence contradiction by RELAT_1:def_9; ::_thesis: verum
end;
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
proof
percases ( i in dom A or not i in dom A ) ;
suppose i in dom A ; ::_thesis: A . i is finite
then A . i in bool F by PARTFUN1:4;
hence A . i is finite ; ::_thesis: verum
end;
suppose not i in dom A ; ::_thesis: A . i is finite
hence A . i is finite by FUNCT_1:def_2; ::_thesis: verum
end;
end;
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
ex b1 being set st
for x being set holds
( x in b1 iff ex j being set st
( j in J & j in dom A & x in A . j ) )
proof
defpred S1[ set ] means ex j being set st
( j in J & j in dom A & $1 in A . j );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in F & S1[x] ) ) from XBOOLE_0:sch_1();
take X ; ::_thesis: for x being set holds
( x in X iff ex j being set st
( j in J & j in dom A & x in A . j ) )
let x be set ; ::_thesis: ( x in X iff ex j being set st
( j in J & j in dom A & x in A . j ) )
thus ( x in X implies ex j being set st
( j in J & j in dom A & x in A . j ) ) by A1; ::_thesis: ( ex j being set st
( j in J & j in dom A & x in A . j ) implies x in X )
given j being set such that A2: j in J and
A3: j in dom A and
A4: x in A . j ; ::_thesis: x in X
( rng A c= bool F & A . j in rng A ) by A3, FINSEQ_1:def_4, FUNCT_1:3;
hence x in X by A1, A2, A3, A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex j being set st
( j in J & j in dom A & x in A . j ) ) ) & ( for x being set 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
defpred S1[ set ] means ex j being set st
( j in J & j in dom A & $1 in A . j );
let A1, A2 be set ; ::_thesis: ( ( for x being set holds
( x in A1 iff ex j being set st
( j in J & j in dom A & x in A . j ) ) ) & ( for x being set holds
( x in A2 iff ex j being set st
( j in J & j in dom A & x in A . j ) ) ) implies A1 = A2 )
assume that
A5: for x being set holds
( x in A1 iff ex j being set st
( j in J & j in dom A & x in A . j ) ) and
A6: for x being set holds
( x in A2 iff ex j being set st
( j in J & j in dom A & x in A . j ) ) ; ::_thesis: A1 = A2
A7: for x being set holds
( x in A2 iff S1[x] ) by A6;
A8: for x being set holds
( x in A1 iff S1[x] ) by A5;
A1 = A2 from XBOOLE_0:sch_2(A8, A7);
hence A1 = A2 ; ::_thesis: verum
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 set 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
let F be set ; ::_thesis: for A being FinSequence of bool F
for J being set holds union (A,J) c= F
let A be FinSequence of bool F; ::_thesis: for J being set holds union (A,J) c= F
let J be set ; ::_thesis: union (A,J) c= F
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (A,J) or x in F )
assume x in union (A,J) ; ::_thesis: x in F
then consider j being set such that
j in J and
A1: j in dom A and
A2: x in A . j by Def1;
( rng A c= bool F & A . j in rng A ) by A1, FINSEQ_1:def_4, FUNCT_1:3;
hence x in F by A2; ::_thesis: verum
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
let F be finite set ; ::_thesis: for A being FinSequence of bool F
for J, K being set st J c= K holds
union (A,J) c= union (A,K)
let A be FinSequence of bool F; ::_thesis: for J, K being set st J c= K holds
union (A,J) c= union (A,K)
let J, K be set ; ::_thesis: ( J c= K implies union (A,J) c= union (A,K) )
assume A1: J c= K ; ::_thesis: union (A,J) c= union (A,K)
thus union (A,J) c= union (A,K) ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union (A,J) or a in union (A,K) )
assume a in union (A,J) ; ::_thesis: a in union (A,K)
then ex j being set st
( j in J & j in dom A & a in A . j ) by Def1;
hence a in union (A,K) by A1, Def1; ::_thesis: verum
end;
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
let F be finite set ; ::_thesis: for A being FinSequence of bool F
for i being Element of NAT st i in dom A holds
union (A,{i}) = A . i
let A be FinSequence of bool F; ::_thesis: for i being Element of NAT st i in dom A holds
union (A,{i}) = A . i
let i be Element of NAT ; ::_thesis: ( i in dom A implies union (A,{i}) = A . i )
assume A1: i in dom A ; ::_thesis: union (A,{i}) = A . i
thus union (A,{i}) c= A . i :: according to XBOOLE_0:def_10 ::_thesis: A . i c= union (A,{i})
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (A,{i}) or x in A . i )
assume x in union (A,{i}) ; ::_thesis: x in A . i
then ex j being set st
( j in {i} & j in dom A & x in A . j ) by Def1;
hence x in A . i by TARSKI:def_1; ::_thesis: verum
end;
thus A . i c= union (A,{i}) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A . i or x in union (A,{i}) )
A2: i in {i} by TARSKI:def_1;
assume x in A . i ; ::_thesis: x in union (A,{i})
hence x in union (A,{i}) by A1, A2, Def1; ::_thesis: verum
end;
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
let F be finite set ; ::_thesis: 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)
let A be FinSequence of bool F; ::_thesis: 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)
let i, j be Element of NAT ; ::_thesis: ( i in dom A & j in dom A implies union (A,{i,j}) = (A . i) \/ (A . j) )
assume that
A1: i in dom A and
A2: j in dom A ; ::_thesis: union (A,{i,j}) = (A . i) \/ (A . j)
thus union (A,{i,j}) c= (A . i) \/ (A . j) :: according to XBOOLE_0:def_10 ::_thesis: (A . i) \/ (A . j) c= union (A,{i,j})
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (A,{i,j}) or x in (A . i) \/ (A . j) )
assume x in union (A,{i,j}) ; ::_thesis: x in (A . i) \/ (A . j)
then consider k being set such that
A3: ( k in {i,j} & k in dom A & x in A . k ) by Def1;
percases ( ( k = i & k in dom A & x in A . k ) or ( k = j & k in dom A & x in A . k ) ) by A3, TARSKI:def_2;
suppose ( k = i & k in dom A & x in A . k ) ; ::_thesis: x in (A . i) \/ (A . j)
hence x in (A . i) \/ (A . j) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose ( k = j & k in dom A & x in A . k ) ; ::_thesis: x in (A . i) \/ (A . j)
hence x in (A . i) \/ (A . j) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
thus (A . i) \/ (A . j) c= union (A,{i,j}) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A . i) \/ (A . j) or x in union (A,{i,j}) )
assume A4: x in (A . i) \/ (A . j) ; ::_thesis: x in union (A,{i,j})
percases ( x in A . i or x in A . j ) by A4, XBOOLE_0:def_3;
supposeA5: x in A . i ; ::_thesis: x in union (A,{i,j})
i in {i,j} by TARSKI:def_2;
hence x in union (A,{i,j}) by A1, A5, Def1; ::_thesis: verum
end;
supposeA6: x in A . j ; ::_thesis: x in union (A,{i,j})
j in {i,j} by TARSKI:def_2;
hence x in union (A,{i,j}) by A2, A6, Def1; ::_thesis: verum
end;
end;
end;
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
let J be set ; ::_thesis: 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)
let F be finite set ; ::_thesis: 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)
let A be FinSequence of bool F; ::_thesis: for i being Element of NAT st i in J & i in dom A holds
A . i c= union (A,J)
let i be Element of NAT ; ::_thesis: ( i in J & i in dom A implies A . i c= union (A,J) )
assume A1: ( i in J & i in dom A ) ; ::_thesis: A . i c= union (A,J)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A . i or x in union (A,J) )
assume x in A . i ; ::_thesis: x in union (A,J)
hence x in union (A,J) by A1, Def1; ::_thesis: verum
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
let J be set ; ::_thesis: 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)
let F be finite set ; ::_thesis: 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)
let i be Element of NAT ; ::_thesis: 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)
let A be FinSequence of bool F; ::_thesis: ( i in J & i in dom A implies union (A,J) = (union (A,(J \ {i}))) \/ (A . i) )
assume ( i in J & i in dom A ) ; ::_thesis: union (A,J) = (union (A,(J \ {i}))) \/ (A . i)
then A1: A . i c= union (A,J) by Th7;
thus union (A,J) c= (union (A,(J \ {i}))) \/ (A . i) :: according to XBOOLE_0:def_10 ::_thesis: (union (A,(J \ {i}))) \/ (A . i) c= union (A,J)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (A,J) or x in (union (A,(J \ {i}))) \/ (A . i) )
assume x in union (A,J) ; ::_thesis: x in (union (A,(J \ {i}))) \/ (A . i)
then consider j being set such that
A2: j in J and
A3: j in dom A and
A4: x in A . j by Def1;
percases ( i = j or i <> j ) ;
suppose i = j ; ::_thesis: x in (union (A,(J \ {i}))) \/ (A . i)
hence x in (union (A,(J \ {i}))) \/ (A . i) by A4, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose i <> j ; ::_thesis: x in (union (A,(J \ {i}))) \/ (A . i)
then not j in {i} by TARSKI:def_1;
then j in J \ {i} by A2, XBOOLE_0:def_5;
then x in union (A,(J \ {i})) by A3, A4, Def1;
hence x in (union (A,(J \ {i}))) \/ (A . i) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
thus (union (A,(J \ {i}))) \/ (A . i) c= union (A,J) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (union (A,(J \ {i}))) \/ (A . i) or x in union (A,J) )
assume x in (union (A,(J \ {i}))) \/ (A . i) ; ::_thesis: x in union (A,J)
then A5: ( x in union (A,(J \ {i})) or x in A . i ) by XBOOLE_0:def_3;
percases ( x in union (A,(J \ {i})) or x in union (A,J) ) by A1, A5;
suppose x in union (A,(J \ {i})) ; ::_thesis: x in union (A,J)
then ex j being set st
( j in J \ {i} & j in dom A & x in A . j ) by Def1;
hence x in union (A,J) by Def1; ::_thesis: verum
end;
suppose x in union (A,J) ; ::_thesis: x in union (A,J)
hence x in union (A,J) ; ::_thesis: verum
end;
end;
end;
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
let J1, J2 be set ; ::_thesis: 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)))
let F be finite set ; ::_thesis: 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)))
let i be Element of NAT ; ::_thesis: for A being FinSequence of bool F st i in dom A holds
union (A,(({i} \/ J1) \/ J2)) = (A . i) \/ (union (A,(J1 \/ J2)))
let A be FinSequence of bool F; ::_thesis: ( i in dom A implies union (A,(({i} \/ J1) \/ J2)) = (A . i) \/ (union (A,(J1 \/ J2))) )
assume i in dom A ; ::_thesis: union (A,(({i} \/ J1) \/ J2)) = (A . i) \/ (union (A,(J1 \/ J2)))
then A1: union (A,{i}) = A . i by Th5;
thus union (A,(({i} \/ J1) \/ J2)) c= (A . i) \/ (union (A,(J1 \/ J2))) :: according to XBOOLE_0:def_10 ::_thesis: (A . i) \/ (union (A,(J1 \/ J2))) c= union (A,(({i} \/ J1) \/ J2))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (A,(({i} \/ J1) \/ J2)) or x in (A . i) \/ (union (A,(J1 \/ J2))) )
assume x in union (A,(({i} \/ J1) \/ J2)) ; ::_thesis: x in (A . i) \/ (union (A,(J1 \/ J2)))
then consider j being set such that
A2: j in ({i} \/ J1) \/ J2 and
A3: j in dom A and
A4: x in A . j by Def1;
percases ( i = j or i <> j ) ;
suppose i = j ; ::_thesis: x in (A . i) \/ (union (A,(J1 \/ J2)))
hence x in (A . i) \/ (union (A,(J1 \/ J2))) by A4, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA5: i <> j ; ::_thesis: x in (A . i) \/ (union (A,(J1 \/ J2)))
j in {i} \/ (J1 \/ J2) by A2, XBOOLE_1:4;
then ( j in {i} or j in J1 \/ J2 ) by XBOOLE_0:def_3;
then x in union (A,(J1 \/ J2)) by A3, A4, A5, Def1, TARSKI:def_1;
hence x in (A . i) \/ (union (A,(J1 \/ J2))) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
thus (A . i) \/ (union (A,(J1 \/ J2))) c= union (A,(({i} \/ J1) \/ J2)) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A . i) \/ (union (A,(J1 \/ J2))) or x in union (A,(({i} \/ J1) \/ J2)) )
assume A6: x in (A . i) \/ (union (A,(J1 \/ J2))) ; ::_thesis: x in union (A,(({i} \/ J1) \/ J2))
percases ( x in union (A,{i}) or x in union (A,(J1 \/ J2)) ) by A1, A6, XBOOLE_0:def_3;
suppose x in union (A,{i}) ; ::_thesis: x in union (A,(({i} \/ J1) \/ J2))
then consider j being set such that
A7: j in {i} and
A8: ( j in dom A & x in A . j ) by Def1;
j in {i} \/ (J1 \/ J2) by A7, XBOOLE_0:def_3;
then j in ({i} \/ J1) \/ J2 by XBOOLE_1:4;
hence x in union (A,(({i} \/ J1) \/ J2)) by A8, Def1; ::_thesis: verum
end;
suppose x in union (A,(J1 \/ J2)) ; ::_thesis: x in union (A,(({i} \/ J1) \/ J2))
then consider j being set such that
A9: j in J1 \/ J2 and
A10: ( j in dom A & x in A . j ) by Def1;
j in {i} \/ (J1 \/ J2) by A9, XBOOLE_0:def_3;
then j in ({i} \/ J1) \/ J2 by XBOOLE_1:4;
hence x in union (A,(({i} \/ J1) \/ J2)) by A10, Def1; ::_thesis: verum
end;
end;
end;
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
let F be finite set ; ::_thesis: 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
let A be FinSequence of bool F; ::_thesis: 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
let i be Element of NAT ; ::_thesis: 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
let x, y be set ; ::_thesis: ( x <> y & x in A . i & y in A . i implies ((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i )
assume that
A1: x <> y and
A2: x in A . i and
A3: y in A . i ; ::_thesis: ((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i
A . i c= ((A . i) \ {x}) \/ ((A . i) \ {y})
proof
{} = {y} \ ({y} \/ {}) by XBOOLE_1:46;
then A . i = (A . i) \ ({y} \ {y}) ;
then A . i = ((A . i) \ {y}) \/ ((A . i) /\ {y}) by XBOOLE_1:52;
then A4: A . i = ((A . i) \ {y}) \/ {y} by A3, ZFMISC_1:46;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in A . i or z in ((A . i) \ {x}) \/ ((A . i) \ {y}) )
not x in {y} by A1, TARSKI:def_1;
then A5: x in (A . i) \ {y} by A2, XBOOLE_0:def_5;
assume z in A . i ; ::_thesis: z in ((A . i) \ {x}) \/ ((A . i) \ {y})
then z in (((A . i) \ {x}) \/ {x}) \/ (((A . i) \ {y}) \/ {y}) by A4, XBOOLE_0:def_3;
then z in ((A . i) \ {x}) \/ ({x} \/ ({y} \/ ((A . i) \ {y}))) by XBOOLE_1:4;
then z in ((A . i) \ {x}) \/ (({x} \/ {y}) \/ ((A . i) \ {y})) by XBOOLE_1:4;
then z in (((A . i) \ {x}) \/ ({y} \/ {x})) \/ ((A . i) \ {y}) by XBOOLE_1:4;
then z in ((((A . i) \ {x}) \/ {y}) \/ {x}) \/ ((A . i) \ {y}) by XBOOLE_1:4;
then A6: z in (((A . i) \ {x}) \/ {y}) \/ ({x} \/ ((A . i) \ {y})) by XBOOLE_1:4;
not y in {x} by A1, TARSKI:def_1;
then y in (A . i) \ {x} by A3, XBOOLE_0:def_5;
then z in ((A . i) \ {x}) \/ ({x} \/ ((A . i) \ {y})) by A6, ZFMISC_1:40;
hence z in ((A . i) \ {x}) \/ ((A . i) \ {y}) by A5, ZFMISC_1:40; ::_thesis: verum
end;
hence ((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i by XBOOLE_0:def_10; ::_thesis: verum
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
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
A . i c= F
proof
percases ( i in dom A or not i in dom A ) ;
suppose i in dom A ; ::_thesis: A . i c= F
then A . i in bool F by FINSEQ_2:11;
hence A . i c= F ; ::_thesis: verum
end;
suppose not i in dom A ; ::_thesis: A . i c= F
then A . i = {} by FUNCT_1:def_2;
hence A . i c= F by XBOOLE_1:2; ::_thesis: verum
end;
end;
end;
then reconsider EX = (A . i) \ {x} as Subset of F by XBOOLE_1:1;
set XX = A +* (i,EX);
reconsider XX = A +* (i,EX) as FinSequence of bool F ;
take XX ; ::_thesis: ( dom XX = dom A & ( for k being Element of NAT st k in dom XX holds
( ( i = k implies XX . k = (A . k) \ {x} ) & ( i <> k implies XX . k = A . k ) ) ) )
dom XX = dom A by FUNCT_7:30;
hence ( dom XX = dom A & ( for k being Element of NAT st k in dom XX holds
( ( i = k implies XX . k = (A . k) \ {x} ) & ( i <> k implies XX . k = A . k ) ) ) ) by FUNCT_7:31, FUNCT_7:32; ::_thesis: verum
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
let f1, f2 be FinSequence of bool F; ::_thesis: ( dom f1 = dom A & ( for k being Element of NAT st k in dom f1 holds
( ( i = k implies f1 . k = (A . k) \ {x} ) & ( i <> k implies f1 . k = A . k ) ) ) & dom f2 = dom A & ( for k being Element of NAT st k in dom f2 holds
( ( i = k implies f2 . k = (A . k) \ {x} ) & ( i <> k implies f2 . k = A . k ) ) ) implies f1 = f2 )
assume that
A1: dom f1 = dom A and
A2: for k being Element of NAT st k in dom f1 holds
( ( i = k implies f1 . k = (A . k) \ {x} ) & ( i <> k implies f1 . k = A . k ) ) and
A3: dom f2 = dom A and
A4: for k being Element of NAT st k in dom f2 holds
( ( i = k implies f2 . k = (A . k) \ {x} ) & ( i <> k implies f2 . k = A . k ) ) ; ::_thesis: f1 = f2
for z being Nat st z in dom f1 holds
f1 . z = f2 . z
proof
let z be Nat; ::_thesis: ( z in dom f1 implies f1 . z = f2 . z )
assume A5: z in dom f1 ; ::_thesis: f1 . z = f2 . z
percases ( z = i or z <> i ) ;
supposeA6: z = i ; ::_thesis: f1 . z = f2 . z
then f1 . z = (A . i) \ {x} by A2, A5
.= f2 . z by A1, A3, A4, A5, A6 ;
hence f1 . z = f2 . z ; ::_thesis: verum
end;
supposeA7: z <> i ; ::_thesis: f1 . z = f2 . z
then f1 . z = A . z by A2, A5
.= f2 . z by A1, A3, A4, A5, A7 ;
hence f1 . z = f2 . z ; ::_thesis: verum
end;
end;
end;
hence f1 = f2 by A1, A3, FINSEQ_1:13; ::_thesis: verum
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
let F be finite set ; ::_thesis: 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
let A be FinSequence of bool F; ::_thesis: 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
let i be Element of NAT ; ::_thesis: for x being set st i in dom A & x in A . i holds
card ((Cut (A,i,x)) . i) = (card (A . i)) - 1
let x be set ; ::_thesis: ( i in dom A & x in A . i implies card ((Cut (A,i,x)) . i) = (card (A . i)) - 1 )
set f = Cut (A,i,x);
assume that
A1: i in dom A and
A2: x in A . i ; ::_thesis: card ((Cut (A,i,x)) . i) = (card (A . i)) - 1
i in dom (Cut (A,i,x)) by A1, Def2;
then A3: (Cut (A,i,x)) . i = (A . i) \ {x} by Def2;
{x} c= A . i by A2, ZFMISC_1:31;
then card ((Cut (A,i,x)) . i) = (card (A . i)) - (card {x}) by A3, CARD_2:44
.= (card (A . i)) - 1 by CARD_2:42 ;
hence card ((Cut (A,i,x)) . i) = (card (A . i)) - 1 ; ::_thesis: verum
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
let F be finite set ; ::_thesis: 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}))
let A be FinSequence of bool F; ::_thesis: for i being Element of NAT
for x, J being set holds union ((Cut (A,i,x)),(J \ {i})) = union (A,(J \ {i}))
let i be Element of NAT ; ::_thesis: for x, J being set holds union ((Cut (A,i,x)),(J \ {i})) = union (A,(J \ {i}))
let x, J be set ; ::_thesis: union ((Cut (A,i,x)),(J \ {i})) = union (A,(J \ {i}))
thus union ((Cut (A,i,x)),(J \ {i})) c= union (A,(J \ {i})) :: according to XBOOLE_0:def_10 ::_thesis: union (A,(J \ {i})) c= union ((Cut (A,i,x)),(J \ {i}))
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union ((Cut (A,i,x)),(J \ {i})) or z in union (A,(J \ {i})) )
assume z in union ((Cut (A,i,x)),(J \ {i})) ; ::_thesis: z in union (A,(J \ {i}))
then consider j being set such that
A1: j in J \ {i} and
A2: j in dom (Cut (A,i,x)) and
A3: z in (Cut (A,i,x)) . j by Def1;
not j in {i} by A1, XBOOLE_0:def_5;
then i <> j by TARSKI:def_1;
then A4: z in A . j by A2, A3, Def2;
j in dom A by A2, Def2;
hence z in union (A,(J \ {i})) by A1, A4, Def1; ::_thesis: verum
end;
A5: dom (Cut (A,i,x)) = dom A by Def2;
thus union (A,(J \ {i})) c= union ((Cut (A,i,x)),(J \ {i})) ::_thesis: verum
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union (A,(J \ {i})) or z in union ((Cut (A,i,x)),(J \ {i})) )
assume z in union (A,(J \ {i})) ; ::_thesis: z in union ((Cut (A,i,x)),(J \ {i}))
then consider j being set such that
A6: j in J \ {i} and
A7: j in dom A and
A8: z in A . j by Def1;
not j in {i} by A6, XBOOLE_0:def_5;
then i <> j by TARSKI:def_1;
then (Cut (A,i,x)) . j = A . j by A5, A7, Def2;
hence z in union ((Cut (A,i,x)),(J \ {i})) by A5, A6, A7, A8, Def1; ::_thesis: verum
end;
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
let F be finite set ; ::_thesis: 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)
let A be FinSequence of bool F; ::_thesis: 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)
let i be Element of NAT ; ::_thesis: for x, J being set st not i in J holds
union (A,J) = union ((Cut (A,i,x)),J)
let x, J be set ; ::_thesis: ( not i in J implies union (A,J) = union ((Cut (A,i,x)),J) )
assume A1: not i in J ; ::_thesis: union (A,J) = union ((Cut (A,i,x)),J)
thus union (A,J) c= union ((Cut (A,i,x)),J) :: according to XBOOLE_0:def_10 ::_thesis: union ((Cut (A,i,x)),J) c= union (A,J)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union (A,J) or z in union ((Cut (A,i,x)),J) )
assume z in union (A,J) ; ::_thesis: z in union ((Cut (A,i,x)),J)
then consider j being set such that
A2: j in J and
A3: j in dom A and
A4: z in A . j by Def1;
A5: j in dom (Cut (A,i,x)) by A3, Def2;
percases ( i = j or i <> j ) ;
suppose i = j ; ::_thesis: z in union ((Cut (A,i,x)),J)
hence z in union ((Cut (A,i,x)),J) by A1, A2; ::_thesis: verum
end;
suppose i <> j ; ::_thesis: z in union ((Cut (A,i,x)),J)
then (Cut (A,i,x)) . j = A . j by A5, Def2;
hence z in union ((Cut (A,i,x)),J) by A2, A4, A5, Def1; ::_thesis: verum
end;
end;
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union ((Cut (A,i,x)),J) or z in union (A,J) )
assume z in union ((Cut (A,i,x)),J) ; ::_thesis: z in union (A,J)
then consider j being set such that
A6: j in J and
A7: j in dom (Cut (A,i,x)) and
A8: z in (Cut (A,i,x)) . j by Def1;
A9: j in dom A by A7, Def2;
percases ( i = j or i <> j ) ;
suppose i = j ; ::_thesis: z in union (A,J)
hence z in union (A,J) by A1, A6; ::_thesis: verum
end;
suppose i <> j ; ::_thesis: z in union (A,J)
then (Cut (A,i,x)) . j = A . j by A7, Def2;
hence z in union (A,J) by A6, A8, A9, Def1; ::_thesis: verum
end;
end;
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
let F be finite set ; ::_thesis: 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})
let A be FinSequence of bool F; ::_thesis: 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})
let i be Element of NAT ; ::_thesis: 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})
let x, J be set ; ::_thesis: ( i in dom (Cut (A,i,x)) & i in J implies union ((Cut (A,i,x)),J) = (union (A,(J \ {i}))) \/ ((A . i) \ {x}) )
assume that
A1: i in dom (Cut (A,i,x)) and
A2: i in J ; ::_thesis: union ((Cut (A,i,x)),J) = (union (A,(J \ {i}))) \/ ((A . i) \ {x})
union ((Cut (A,i,x)),J) = (union ((Cut (A,i,x)),(J \ {i}))) \/ ((Cut (A,i,x)) . i) by A1, A2, Th8
.= (union (A,(J \ {i}))) \/ ((Cut (A,i,x)) . i) by Th12
.= (union (A,(J \ {i}))) \/ ((A . i) \ {x}) by A1, Def2 ;
hence union ((Cut (A,i,x)),J) = (union (A,(J \ {i}))) \/ ((A . i) \ {x}) ; ::_thesis: verum
end;
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 & 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_:_
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;
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 & not b1 is empty )
proof
set c = the Element of F;
reconsider b = { the Element of F} as Element of bool F by ZFMISC_1:31;
reconsider f = <*b*> as FinSequence of bool F ;
for J being finite set st J c= dom f holds
card J <= card (union (f,J))
proof
let J be finite set ; ::_thesis: ( J c= dom f implies card J <= card (union (f,J)) )
assume A1: J c= dom f ; ::_thesis: card J <= card (union (f,J))
A2: dom f = {1} by FINSEQ_1:2, FINSEQ_1:38;
then A3: ( J = {} or J = {1} ) by A1, ZFMISC_1:33;
percases ( J = {} or J = {1} ) by A3;
suppose J = {} ; ::_thesis: card J <= card (union (f,J))
then card J = 0 ;
hence card J <= card (union (f,J)) by NAT_1:2; ::_thesis: verum
end;
supposeA4: J = {1} ; ::_thesis: card J <= card (union (f,J))
( 1 in dom f & 1 in NAT ) by A2, TARSKI:def_1;
then union (f,{1}) = f . 1 by Th5
.= b by FINSEQ_1:40 ;
then card (union (f,J)) = 1 by A4, CARD_1:30;
hence card J <= card (union (f,J)) by A4, CARD_1:30; ::_thesis: verum
end;
end;
end;
then f is Hall by Def4;
hence ex b1 being FinSequence of bool F st
( b1 is Hall & not b1 is empty ) ; ::_thesis: verum
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 b1 being FinSequence of bool F st b1 is Hall
proof
reconsider f = <*> (bool F) as FinSequence of bool F ;
for J being finite set st J c= dom f holds
card J <= card (union (f,J))
proof
let J be finite set ; ::_thesis: ( J c= dom f implies card J <= card (union (f,J)) )
assume J c= dom f ; ::_thesis: card J <= card (union (f,J))
then card J = 0 ;
hence card J <= card (union (f,J)) by NAT_1:2; ::_thesis: verum
end;
then A1: f is Hall by Def4;
take f ; ::_thesis: f is Hall
thus f is Hall by A1; ::_thesis: verum
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
let F be finite set ; ::_thesis: for A being non empty FinSequence of bool F st A is Hall holds
A is non-empty
let A be non empty FinSequence of bool F; ::_thesis: ( A is Hall implies A is non-empty )
assume A1: A is Hall ; ::_thesis: A is non-empty
assume not A is non-empty ; ::_thesis: contradiction
then {} in rng A by RELAT_1:def_9;
then consider i being set such that
A2: ( i in dom A & A . i = {} ) by FUNCT_1:def_3;
set J = {i};
A3: card {i} = 1 by CARD_2:42;
( {i} c= dom A & card (union (A,{i})) = 0 ) by A2, Th5, CARD_1:27, ZFMISC_1:31;
hence contradiction by A1, A3, Def4; ::_thesis: verum
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
let F be finite set ; ::_thesis: 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
let A be FinSequence of bool F; ::_thesis: for i being Element of NAT st i in dom A & A is Hall holds
card (A . i) >= 1
let i be Element of NAT ; ::_thesis: ( i in dom A & A is Hall implies card (A . i) >= 1 )
assume that
A1: i in dom A and
A2: A is Hall ; ::_thesis: card (A . i) >= 1
set J = {i};
{i} c= dom A by A1, ZFMISC_1:31;
then A3: card {i} <= card (union (A,{i})) by A2, Def4;
assume A4: card (A . i) < 1 ; ::_thesis: contradiction
union (A,{i}) = A . i by A1, Th5;
hence contradiction by A4, A3, CARD_2:42; ::_thesis: verum
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
let F be non empty finite set ; ::_thesis: 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
let A be non empty FinSequence of bool F; ::_thesis: ( ( for i being Element of NAT st i in dom A holds
card (A . i) = 1 ) & A is Hall implies ex X being set st X is_a_system_of_different_representatives_of A )
assume A1: for i being Element of NAT st i in dom A holds
card (A . i) = 1 ; ::_thesis: ( not A is Hall or ex X being set st X is_a_system_of_different_representatives_of A )
reconsider dA = dom A as non empty set ;
deffunc H1( Element of dA) -> set = A . $1;
assume A2: A is Hall ; ::_thesis: ex X being set st X is_a_system_of_different_representatives_of A
A3: for a being Element of dA holds F meets H1(a)
proof
let a be Element of dA; ::_thesis: F meets H1(a)
set z = the Element of A . a;
A . a <> {} by A2;
then A4: the Element of A . a in A . a ;
( rng A c= bool F & A . a in rng A ) by FINSEQ_1:def_4, FUNCT_1:3;
hence F meets H1(a) by A4, XBOOLE_0:3; ::_thesis: verum
end;
ex f being Function of dA,F st
for a being Element of dA holds f . a in H1(a) from FUNCT_2:sch_10(A3);
then consider f being Function of dA,F such that
A5: for a being Element of dA holds f . a in H1(a) ;
A6: dom f = dom A by FUNCT_2:def_1;
A7: rng f c= F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in F )
A8: rng A c= bool F by FINSEQ_1:def_4;
assume x in rng f ; ::_thesis: x in F
then consider y being set such that
A9: y in dom f and
A10: x = f . y by FUNCT_1:def_3;
( f . y in A . y & A . y in rng A ) by A5, A6, A9, FUNCT_1:3;
hence x in F by A10, A8; ::_thesis: verum
end;
ex n being Nat st dom A = Seg n by FINSEQ_1:def_2;
then f is FinSequence by A6, FINSEQ_1:def_2;
then reconsider f = f as FinSequence of F by A7, FINSEQ_1:def_4;
A11: dom A = dom f by FUNCT_2:def_1;
A12: card {{}} = 1 by CARD_1:30;
for i, j being Element of NAT st i in dom f & j in dom f & i <> j holds
f . i <> f . j
proof
let i, j be Element of NAT ; ::_thesis: ( i in dom f & j in dom f & i <> j implies f . i <> f . j )
assume that
A13: i in dom f and
A14: j in dom f and
A15: i <> j ; ::_thesis: f . i <> f . j
thus f . i <> f . j ::_thesis: verum
proof
card (A . i) = card {{}} by A1, A12, A11, A13;
then consider y being set such that
A16: A . i = {y} by CARD_1:29;
A17: A . i = {(f . i)}
proof
thus A . i c= {(f . i)} :: according to XBOOLE_0:def_10 ::_thesis: {(f . i)} c= A . i
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A . i or x in {(f . i)} )
assume A18: x in A . i ; ::_thesis: x in {(f . i)}
x = f . i
proof
f . i in A . i by A5, A6, A13;
then A19: f . i = y by A16, TARSKI:def_1;
assume x <> f . i ; ::_thesis: contradiction
hence contradiction by A16, A18, A19, TARSKI:def_1; ::_thesis: verum
end;
hence x in {(f . i)} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(f . i)} or x in A . i )
assume x in {(f . i)} ; ::_thesis: x in A . i
then x = f . i by TARSKI:def_1;
hence x in A . i by A5, A6, A13; ::_thesis: verum
end;
A20: j in dom A by A14, FUNCT_2:def_1;
then card (A . j) = card {{}} by A1, A12;
then consider z being set such that
A21: A . j = {z} by CARD_1:29;
A22: A . j = {(f . j)}
proof
thus A . j c= {(f . j)} :: according to XBOOLE_0:def_10 ::_thesis: {(f . j)} c= A . j
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A . j or x in {(f . j)} )
assume A23: x in A . j ; ::_thesis: x in {(f . j)}
x = f . j
proof
f . j in A . j by A5, A6, A14;
then A24: f . j = z by A21, TARSKI:def_1;
assume x <> f . j ; ::_thesis: contradiction
hence contradiction by A21, A23, A24, TARSKI:def_1; ::_thesis: verum
end;
hence x in {(f . j)} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(f . j)} or x in A . j )
assume x in {(f . j)} ; ::_thesis: x in A . j
then x = f . j by TARSKI:def_1;
hence x in A . j by A5, A6, A14; ::_thesis: verum
end;
set J = {i,j};
assume f . i = f . j ; ::_thesis: contradiction
then A25: {(f . i),(f . j)} = {(f . i)} by ENUMSET1:29;
A26: card {i,j} = 2 by A15, CARD_2:57;
A27: i in dom A by A13, FUNCT_2:def_1;
then A28: {i,j} c= dom A by A20, ZFMISC_1:32;
card (union (A,{i,j})) = card ((A . i) \/ (A . j)) by A27, A20, Th6
.= card {(f . i),(f . j)} by A17, A22, ENUMSET1:1
.= 1 by A25, CARD_1:30 ;
hence contradiction by A2, A26, A28, Def4; ::_thesis: verum
end;
end;
then for i, j being set st i in dom f & j in dom f & f . i = f . j holds
i = j ;
then A29: f is one-to-one by FUNCT_1:def_4;
for i being Element of NAT st i in dom f holds
f . i in A . i by A5, A6;
then f is_a_system_of_different_representatives_of A by A11, A29, Def3;
hence ex X being set st X is_a_system_of_different_representatives_of A ; ::_thesis: verum
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
let F be finite set ; ::_thesis: 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
let A be FinSequence of bool F; ::_thesis: ( ex X being set st X is_a_system_of_different_representatives_of A implies A is Hall )
given X being set such that A1: X is_a_system_of_different_representatives_of A ; ::_thesis: A is Hall
consider f being FinSequence of F such that
f = X and
A2: dom A = dom f and
A3: for i being Element of NAT st i in dom f holds
f . i in A . i and
A4: f is one-to-one by A1, Def3;
for J being finite set st J c= dom A holds
card J <= card (union (A,J))
proof
let J be finite set ; ::_thesis: ( J c= dom A implies card J <= card (union (A,J)) )
set X = J;
set Y = union (A,J);
set g = f | J;
assume A5: J c= dom A ; ::_thesis: card J <= card (union (A,J))
then A6: dom (f | J) = J by A2, RELAT_1:62;
A7: dom (f | J) c= dom f by RELAT_1:60;
A8: rng (f | J) c= union (A,J)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (f | J) or x in union (A,J) )
assume x in rng (f | J) ; ::_thesis: x in union (A,J)
then consider a being set such that
A9: a in dom (f | J) and
A10: x = (f | J) . a by FUNCT_1:def_3;
a in dom f by A7, A9;
then reconsider a = a as Element of NAT ;
f . a in A . a by A2, A3, A5, A6, A9;
then (f | J) . a in A . a by A9, FUNCT_1:47;
hence x in union (A,J) by A5, A6, A9, A10, Def1; ::_thesis: verum
end;
f | J is one-to-one by A4, FUNCT_1:52;
then card J c= card (union (A,J)) by A6, A8, CARD_1:10;
hence card J <= card (union (A,J)) by NAT_1:39; ::_thesis: verum
end;
hence A is Hall by Def4; ::_thesis: verum
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
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
take A ; ::_thesis: ( dom A = dom A & ( for j being Element of NAT st j in dom A & j <> i holds
A . j = A . j ) & A . i c= A . i )
thus ( dom A = dom A & ( for j being Element of NAT st j in dom A & j <> i holds
A . j = A . j ) & A . i c= A . i ) ; ::_thesis: verum
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
for i being Element of NAT st i in dom A holds
A . i c= A . i ;
hence 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 ) ) ; ::_thesis: verum
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 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
proof
set x = the Element of A . i;
( A . i in bool F & the Element of A . i in A . i ) by A1, A2, PARTFUN1:4;
then reconsider E = { the Element of A . i} as Subset of F by ZFMISC_1:31;
reconsider G = A +* (i,E) as FinSequence of bool F ;
A3: for j being Element of NAT st j in dom A holds
G . j c= A . j
proof
let j be Element of NAT ; ::_thesis: ( j in dom A implies G . j c= A . j )
assume j in dom A ; ::_thesis: G . j c= A . j
percases ( j = i or j <> i ) ;
supposeA4: j = i ; ::_thesis: G . j c= A . j
G . i = { the Element of A . i} by A1, FUNCT_7:31;
hence G . j c= A . j by A2, A4, ZFMISC_1:31; ::_thesis: verum
end;
suppose j <> i ; ::_thesis: G . j c= A . j
hence G . j c= A . j by FUNCT_7:32; ::_thesis: verum
end;
end;
end;
G . i = { the Element of A . i} by A1, FUNCT_7:31;
then A5: card (G . i) = 1 by CARD_2:42;
dom G = dom A by FUNCT_7:30;
then G is Reduction of A by A3, Def6;
hence ex b1 being Reduction of A st card (b1 . i) = 1 by A5; ::_thesis: verum
end;
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 & 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
let F be finite set ; ::_thesis: 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
let A be FinSequence of bool F; ::_thesis: for i being Element of NAT
for C being Reduction of A,i holds C is Reduction of A
let i be Element of NAT ; ::_thesis: for C being Reduction of A,i holds C is Reduction of A
let C be Reduction of A,i; ::_thesis: C is Reduction of A
A1: dom C = dom A by Def5;
for j being Element of NAT st j in dom C holds
C . j c= A . j
proof
let j be Element of NAT ; ::_thesis: ( j in dom C implies C . j c= A . j )
assume A2: j in dom C ; ::_thesis: C . j c= A . j
percases ( j = i or j <> i ) ;
suppose j = i ; ::_thesis: C . j c= A . j
hence C . j c= A . j by Def5; ::_thesis: verum
end;
suppose j <> i ; ::_thesis: C . j c= A . j
hence C . j c= A . j by A1, A2, Def5; ::_thesis: verum
end;
end;
end;
hence C is Reduction of A by A1, Def6; ::_thesis: verum
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
let F be finite set ; ::_thesis: 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
let A be FinSequence of bool F; ::_thesis: 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
let i be Element of NAT ; ::_thesis: for x being set st i in dom A holds
Cut (A,i,x) is Reduction of A,i
let x be set ; ::_thesis: ( i in dom A implies Cut (A,i,x) is Reduction of A,i )
set f = Cut (A,i,x);
A1: dom (Cut (A,i,x)) = dom A by Def2;
then A2: for j being Element of NAT st j in dom A & j <> i holds
A . j = (Cut (A,i,x)) . j by Def2;
assume i in dom A ; ::_thesis: Cut (A,i,x) is Reduction of A,i
then (Cut (A,i,x)) . i = (A . i) \ {x} by A1, Def2;
hence Cut (A,i,x) is Reduction of A,i by A1, A2, Def5; ::_thesis: verum
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
let F be finite set ; ::_thesis: 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
let A be FinSequence of bool F; ::_thesis: for i being Element of NAT
for x being set st i in dom A holds
Cut (A,i,x) is Reduction of A
let i be Element of NAT ; ::_thesis: for x being set st i in dom A holds
Cut (A,i,x) is Reduction of A
let x be set ; ::_thesis: ( i in dom A implies Cut (A,i,x) is Reduction of A )
assume i in dom A ; ::_thesis: Cut (A,i,x) is Reduction of A
then Cut (A,i,x) is Reduction of A,i by Th20;
hence Cut (A,i,x) is Reduction of A by Th19; ::_thesis: verum
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
let F be finite set ; ::_thesis: 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
let A be FinSequence of bool F; ::_thesis: for B being Reduction of A
for C being Reduction of B holds C is Reduction of A
let B be Reduction of A; ::_thesis: for C being Reduction of B holds C is Reduction of A
let C be Reduction of B; ::_thesis: C is Reduction of A
A1: for i being Element of NAT st i in dom A holds
C . i c= A . i
proof
let i be Element of NAT ; ::_thesis: ( i in dom A implies C . i c= A . i )
assume A2: i in dom A ; ::_thesis: C . i c= A . i
then i in dom B by Def6;
then A3: C . i c= B . i by Def6;
B . i c= A . i by A2, Def6;
hence C . i c= A . i by A3, XBOOLE_1:1; ::_thesis: verum
end;
dom B = dom C by Def6;
hence C is Reduction of A by A1, Def6; ::_thesis: verum
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
let F be non empty finite set ; ::_thesis: 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 <> {}
let A be non-empty FinSequence of bool F; ::_thesis: for i being Element of NAT
for B being Singlification of A,i st i in dom A holds
B . i <> {}
let i be Element of NAT ; ::_thesis: for B being Singlification of A,i st i in dom A holds
B . i <> {}
let B be Singlification of A,i; ::_thesis: ( i in dom A implies B . i <> {} )
assume A1: i in dom A ; ::_thesis: B . i <> {}
then A . i <> {} by Th2;
hence B . i <> {} by A1, Def7, CARD_1:27; ::_thesis: verum
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
let F be non empty finite set ; ::_thesis: 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 )
let A be non-empty FinSequence of bool F; ::_thesis: 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 )
let i, j be Element of NAT ; ::_thesis: 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 )
let B be Singlification of A,i; ::_thesis: 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 )
let C be Singlification of B,j; ::_thesis: ( i in dom A & j in dom A & C . i <> {} & B . j <> {} implies ( C is Singlification of A,j & C is Singlification of A,i ) )
assume that
A1: i in dom A and
A2: j in dom A and
A3: C . i <> {} and
A4: B . j <> {} ; ::_thesis: ( C is Singlification of A,j & C is Singlification of A,i )
A5: dom B = dom A by Def6;
then A6: C . i c= B . i by A1, Def6;
A7: A . i <> {} by A1, Th2;
then card (B . i) = 1 by A1, Def7;
then A8: card (C . i) = 1 by A3, A6, NAT_1:25, NAT_1:43;
A9: A . j <> {} by A2, Th2;
A10: C is Reduction of A by Th22;
card (C . j) = 1 by A2, A4, A5, Def7;
hence ( C is Singlification of A,j & C is Singlification of A,i ) by A1, A2, A7, A9, A10, A8, Def7; ::_thesis: verum
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
let F be set ; ::_thesis: for A being FinSequence of bool F
for i being Element of NAT holds A is Reduction of A,i
let A be FinSequence of bool F; ::_thesis: for i being Element of NAT holds A is Reduction of A,i
let i be Element of NAT ; ::_thesis: A is Reduction of A,i
( ( for j being Element of NAT st j in dom A & j <> i holds
A . j = A . j ) & A . i c= A . i ) ;
hence A is Reduction of A,i by Def5; ::_thesis: verum
end;
theorem Th26: :: HALLMAR1:26
for F being set
for A being FinSequence of bool F holds A is Reduction of A
proof
let F be set ; ::_thesis: for A being FinSequence of bool F holds A is Reduction of A
let A be FinSequence of bool F; ::_thesis: A is Reduction of A
for i being Element of NAT st i in dom A holds
A . i c= A . i ;
hence A is Reduction of A by Def6; ::_thesis: verum
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
deffunc H1( set ) -> set = {(choose (A . $1))};
A2: for x being set st x in dom A holds
H1(x) in bool F
proof
let x be set ; ::_thesis: ( x in dom A implies H1(x) in bool F )
assume A3: x in dom A ; ::_thesis: H1(x) in bool F
then A . x <> {} by A1, Th2;
then A4: {(choose (A . x))} c= A . x by ZFMISC_1:31;
A . x in bool F by A3, PARTFUN1:4;
then {(choose (A . x))} c= F by A4, XBOOLE_1:1;
hence H1(x) in bool F ; ::_thesis: verum
end;
ex f being Function of (dom A),(bool F) st
for x being set st x in dom A holds
f . x = H1(x) from FUNCT_2:sch_2(A2);
then consider f being Function of (dom A),(bool F) such that
A5: for x being set st x in dom A holds
f . x = H1(x) ;
A6: for i being Element of NAT st i in dom f holds
f . i = {(choose (A . i))}
proof
let i be Element of NAT ; ::_thesis: ( i in dom f implies f . i = {(choose (A . i))} )
assume i in dom f ; ::_thesis: f . i = {(choose (A . i))}
then i in dom A by FUNCT_2:def_1;
hence f . i = {(choose (A . i))} by A5; ::_thesis: verum
end;
A7: dom f = dom A by FUNCT_2:def_1;
A8: for i being Element of NAT st i in dom A holds
f . i c= A . i
proof
let i be Element of NAT ; ::_thesis: ( i in dom A implies f . i c= A . i )
assume A9: i in dom A ; ::_thesis: f . i c= A . i
then A . i <> {} by A1, Th2;
then {(choose (A . i))} c= A . i by ZFMISC_1:31;
hence f . i c= A . i by A7, A6, A9; ::_thesis: verum
end;
dom f = dom A by FUNCT_2:def_1
.= Seg (len A) by FINSEQ_1:def_3 ;
then A10: f is FinSequence by FINSEQ_1:def_2;
rng f c= bool F by RELAT_1:def_19;
then f is FinSequence of bool F by A10, FINSEQ_1:def_4;
then reconsider f = f as Reduction of A by A7, A8, Def6;
for i being Element of NAT st i in dom A holds
card (f . i) = 1
proof
let i be Element of NAT ; ::_thesis: ( i in dom A implies card (f . i) = 1 )
assume i in dom A ; ::_thesis: card (f . i) = 1
then i in dom f by FUNCT_2:def_1;
then f . i = {(choose (A . i))} by A6;
hence card (f . i) = 1 by CARD_2:42; ::_thesis: verum
end;
hence ex b1 being Reduction of A st
for i being Element of NAT st i in dom A holds
card (b1 . i) = 1 ; ::_thesis: verum
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
let F be non empty finite set ; ::_thesis: 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 ) ) )
let A be non empty non-empty FinSequence of bool F; ::_thesis: 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 ) ) )
let f be Function; ::_thesis: ( 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 ) ) )
hereby ::_thesis: ( dom f = dom A & ( for i being Element of NAT st i in dom A holds
f is Singlification of A,i ) implies f is Singlification of A )
assume f is Singlification of A ; ::_thesis: ( dom f = dom A & ( for i being Element of NAT st i in dom A holds
f is Singlification of A,i ) )
then reconsider f9 = f as Singlification of A ;
f9 is Reduction of A ;
hence dom f = dom A by Def6; ::_thesis: for i being Element of NAT st i in dom A holds
f is Singlification of A,i
let i be Element of NAT ; ::_thesis: ( i in dom A implies f is Singlification of A,i )
assume A1: i in dom A ; ::_thesis: f is Singlification of A,i
then ( card (f9 . i) = 1 & A . i <> {} ) by Def8;
hence f is Singlification of A,i by A1, Def7; ::_thesis: verum
end;
assume that
A2: dom f = dom A and
A3: for i being Element of NAT st i in dom A holds
f is Singlification of A,i ; ::_thesis: f is Singlification of A
reconsider f = f as FinSequence of bool F by A3, FINSEQ_5:6;
for i being Element of NAT st i in dom A holds
f . i c= A . i
proof
let i be Element of NAT ; ::_thesis: ( i in dom A implies f . i c= A . i )
assume A4: i in dom A ; ::_thesis: f . i c= A . i
then f is Singlification of A,i by A3;
hence f . i c= A . i by A4, Def6; ::_thesis: verum
end;
then reconsider f9 = f as Reduction of A by A2, Def6;
for i being Element of NAT st i in dom A holds
card (f9 . i) = 1
proof
let i be Element of NAT ; ::_thesis: ( i in dom A implies card (f9 . i) = 1 )
assume A5: i in dom A ; ::_thesis: card (f9 . i) = 1
then ( f is Singlification of A,i & A . i <> {} ) by A3;
hence card (f9 . i) = 1 by A5, Def7; ::_thesis: verum
end;
hence f is Singlification of A by Def8; ::_thesis: verum
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
let G be Singlification of A,k; ::_thesis: not G is empty
dom G = dom A by Def6;
hence not G is empty ; ::_thesis: verum
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
let G be Singlification of A; ::_thesis: not G is empty
dom G = dom A by Def6;
hence not G is empty ; ::_thesis: verum
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
let F be non empty finite set ; ::_thesis: 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
let A be non empty FinSequence of bool F; ::_thesis: 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
let X be set ; ::_thesis: 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
let B be Reduction of A; ::_thesis: ( X is_a_system_of_different_representatives_of B implies X is_a_system_of_different_representatives_of A )
assume A1: X is_a_system_of_different_representatives_of B ; ::_thesis: X is_a_system_of_different_representatives_of A
X is_a_system_of_different_representatives_of A
proof
consider f being FinSequence of F such that
A2: f = X and
A3: dom B = dom f and
A4: for i being Element of NAT st i in dom f holds
f . i in B . i and
A5: f is one-to-one by A1, Def3;
A6: for i being Element of NAT st i in dom f holds
f . i in A . i
proof
let i be Element of NAT ; ::_thesis: ( i in dom f implies f . i in A . i )
assume A7: i in dom f ; ::_thesis: f . i in A . i
A8: f . i in B . i by A4, A7;
dom B = dom A by Def6;
then B . i c= A . i by A3, A7, Def6;
hence f . i in A . i by A8; ::_thesis: verum
end;
dom A = dom B by Def6;
hence X is_a_system_of_different_representatives_of A by A2, A3, A5, A6, Def3; ::_thesis: verum
end;
hence X is_a_system_of_different_representatives_of A ; ::_thesis: verum
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
let F be finite set ; ::_thesis: 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 )
let A be FinSequence of bool F; ::_thesis: ( A is Hall implies 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 ) )
assume A1: A is Hall ; ::_thesis: 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 )
let i be Element of NAT ; ::_thesis: ( card (A . i) >= 2 implies ex x being set st
( x in A . i & Cut (A,i,x) is Hall ) )
assume A2: card (A . i) >= 2 ; ::_thesis: ex x being set st
( x in A . i & Cut (A,i,x) is Hall )
2 c= card (A . i) by A2, NAT_1:39;
then reconsider Ai = A . i as non trivial finite set by PENCIL_1:4;
consider x, y being set such that
A3: x in Ai and
A4: y in Ai and
A5: x <> y by ZFMISC_1:def_10;
assume A6: for z being set st z in A . i holds
not Cut (A,i,z) is Hall ; ::_thesis: contradiction
then not Cut (A,i,x) is Hall by A3;
then consider JJ1 being finite set such that
A7: JJ1 c= dom (Cut (A,i,x)) and
A8: card JJ1 > card (union ((Cut (A,i,x)),JJ1)) by Def4;
ex J1 being finite set st
( not i in J1 & J1 c= dom (Cut (A,i,x)) & card J1 >= card ((union (A,J1)) \/ ((A . i) \ {x})) )
proof
percases ( i in JJ1 or not i in JJ1 ) ;
supposeA9: i in JJ1 ; ::_thesis: ex J1 being finite set st
( not i in J1 & J1 c= dom (Cut (A,i,x)) & card J1 >= card ((union (A,J1)) \/ ((A . i) \ {x})) )
set J1 = JJ1 \ {i};
A10: card (JJ1 \ {i}) = (card JJ1) - (card {i}) by A9, EULER_1:4
.= (card JJ1) - 1 by CARD_1:30 ;
A11: ( JJ1 \ {i} c= dom (Cut (A,i,x)) & {i} misses JJ1 \ {i} ) by A7, XBOOLE_1:1, XBOOLE_1:79;
union ((Cut (A,i,x)),JJ1) = (union (A,(JJ1 \ {i}))) \/ ((A . i) \ {x}) by A7, A9, Th14;
then card (JJ1 \ {i}) >= card ((union (A,(JJ1 \ {i}))) \/ ((A . i) \ {x})) by A8, A10, SPPOL_1:1;
hence ex J1 being finite set st
( not i in J1 & J1 c= dom (Cut (A,i,x)) & card J1 >= card ((union (A,J1)) \/ ((A . i) \ {x})) ) by A11, ZFMISC_1:48; ::_thesis: verum
end;
supposeA12: not i in JJ1 ; ::_thesis: ex J1 being finite set st
( not i in J1 & J1 c= dom (Cut (A,i,x)) & card J1 >= card ((union (A,J1)) \/ ((A . i) \ {x})) )
take J1 = JJ1; ::_thesis: ( not i in J1 & J1 c= dom (Cut (A,i,x)) & card J1 >= card ((union (A,J1)) \/ ((A . i) \ {x})) )
A13: J1 c= dom A by A7, Def2;
card J1 > card (union (A,J1)) by A8, A12, Th13;
hence ( not i in J1 & J1 c= dom (Cut (A,i,x)) & card J1 >= card ((union (A,J1)) \/ ((A . i) \ {x})) ) by A1, A13, Def4; ::_thesis: verum
end;
end;
end;
then consider J1 being finite set such that
A14: not i in J1 and
A15: J1 c= dom (Cut (A,i,x)) and
A16: card J1 >= card ((union (A,J1)) \/ ((A . i) \ {x})) ;
not Cut (A,i,y) is Hall by A4, A6;
then consider JJ2 being finite set such that
A17: JJ2 c= dom (Cut (A,i,y)) and
A18: card JJ2 > card (union ((Cut (A,i,y)),JJ2)) by Def4;
ex J2 being finite set st
( not i in J2 & J2 c= dom (Cut (A,i,y)) & card J2 >= card ((union (A,J2)) \/ ((A . i) \ {y})) )
proof
percases ( i in JJ2 or not i in JJ2 ) ;
supposeA19: i in JJ2 ; ::_thesis: ex J2 being finite set st
( not i in J2 & J2 c= dom (Cut (A,i,y)) & card J2 >= card ((union (A,J2)) \/ ((A . i) \ {y})) )
set J2 = JJ2 \ {i};
A20: card (JJ2 \ {i}) = (card JJ2) - (card {i}) by A19, EULER_1:4
.= (card JJ2) - 1 by CARD_1:30 ;
A21: ( JJ2 \ {i} c= dom (Cut (A,i,y)) & {i} misses JJ2 \ {i} ) by A17, XBOOLE_1:1, XBOOLE_1:79;
union ((Cut (A,i,y)),JJ2) = (union (A,(JJ2 \ {i}))) \/ ((A . i) \ {y}) by A17, A19, Th14;
then card (JJ2 \ {i}) >= card ((union (A,(JJ2 \ {i}))) \/ ((A . i) \ {y})) by A18, A20, SPPOL_1:1;
hence ex J2 being finite set st
( not i in J2 & J2 c= dom (Cut (A,i,y)) & card J2 >= card ((union (A,J2)) \/ ((A . i) \ {y})) ) by A21, ZFMISC_1:48; ::_thesis: verum
end;
supposeA22: not i in JJ2 ; ::_thesis: ex J2 being finite set st
( not i in J2 & J2 c= dom (Cut (A,i,y)) & card J2 >= card ((union (A,J2)) \/ ((A . i) \ {y})) )
set J2 = JJ2;
take JJ2 ; ::_thesis: ( not i in JJ2 & JJ2 c= dom (Cut (A,i,y)) & card JJ2 >= card ((union (A,JJ2)) \/ ((A . i) \ {y})) )
A23: JJ2 c= dom A by A17, Def2;
card JJ2 > card (union (A,JJ2)) by A18, A22, Th13;
hence ( not i in JJ2 & JJ2 c= dom (Cut (A,i,y)) & card JJ2 >= card ((union (A,JJ2)) \/ ((A . i) \ {y})) ) by A1, A23, Def4; ::_thesis: verum
end;
end;
end;
then consider J2 being finite set such that
A24: not i in J2 and
A25: J2 c= dom (Cut (A,i,y)) and
A26: card J2 >= card ((union (A,J2)) \/ ((A . i) \ {y})) ;
reconsider L = {i} \/ (J1 \/ J2) as finite set ;
A27: J2 c= dom A by A25, Def2;
(union (A,(J1 \/ J2))) \/ Ai c= ((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y}))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (union (A,(J1 \/ J2))) \/ Ai or a in ((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y})) )
assume A28: a in (union (A,(J1 \/ J2))) \/ Ai ; ::_thesis: a in ((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y}))
percases ( a in union (A,(J1 \/ J2)) or a in Ai ) by A28, XBOOLE_0:def_3;
suppose a in union (A,(J1 \/ J2)) ; ::_thesis: a in ((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y}))
then consider j being set such that
A29: j in J1 \/ J2 and
A30: ( j in dom A & a in A . j ) by Def1;
( j in J1 or j in J2 ) by A29, XBOOLE_0:def_3;
then ( a in union (A,J1) or a in union (A,J2) ) by A30, Def1;
then a in (union (A,J1)) \/ (union (A,J2)) by XBOOLE_0:def_3;
then a in ((union (A,J1)) \/ (union (A,J2))) \/ ((Ai \ {x}) \/ (Ai \ {y})) by XBOOLE_0:def_3;
then a in (((union (A,J1)) \/ (union (A,J2))) \/ (Ai \ {x})) \/ (Ai \ {y}) by XBOOLE_1:4;
then a in (((union (A,J1)) \/ (Ai \ {x})) \/ (union (A,J2))) \/ (Ai \ {y}) by XBOOLE_1:4;
hence a in ((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y})) by XBOOLE_1:4; ::_thesis: verum
end;
suppose a in Ai ; ::_thesis: a in ((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y}))
then ( a in (Ai \ {x}) \/ (Ai \ {y}) or a in union (A,J1) or a in union (A,J2) ) by A3, A4, A5, Th10;
then ( a in ((Ai \ {x}) \/ (Ai \ {y})) \/ (union (A,J1)) or a in union (A,J2) ) by XBOOLE_0:def_3;
then a in (((Ai \ {x}) \/ (Ai \ {y})) \/ (union (A,J1))) \/ (union (A,J2)) by XBOOLE_0:def_3;
then a in ((union (A,J1)) \/ (union (A,J2))) \/ ((Ai \ {x}) \/ (Ai \ {y})) by XBOOLE_1:4;
then a in (((union (A,J1)) \/ (union (A,J2))) \/ (Ai \ {x})) \/ (Ai \ {y}) by XBOOLE_1:4;
then a in (((union (A,J1)) \/ (Ai \ {x})) \/ (union (A,J2))) \/ (Ai \ {y}) by XBOOLE_1:4;
hence a in ((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y})) by XBOOLE_1:4; ::_thesis: verum
end;
end;
end;
then A31: card (((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y}))) >= card ((union (A,(J1 \/ J2))) \/ Ai) by NAT_1:43;
union (A,(J1 /\ J2)) c= (union (A,J1)) /\ (union (A,J2))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (A,(J1 /\ J2)) or x in (union (A,J1)) /\ (union (A,J2)) )
assume x in union (A,(J1 /\ J2)) ; ::_thesis: x in (union (A,J1)) /\ (union (A,J2))
then consider j being set such that
A32: j in J1 /\ J2 and
A33: ( j in dom A & x in A . j ) by Def1;
j in J2 by A32, XBOOLE_0:def_4;
then A34: x in union (A,J2) by A33, Def1;
j in J1 by A32, XBOOLE_0:def_4;
then x in union (A,J1) by A33, Def1;
hence x in (union (A,J1)) /\ (union (A,J2)) by A34, XBOOLE_0:def_4; ::_thesis: verum
end;
then card ((union (A,J1)) /\ (union (A,J2))) >= card (union (A,(J1 /\ J2))) by NAT_1:43;
then A35: (card ((union (A,(J1 \/ J2))) \/ Ai)) + (card ((union (A,J1)) /\ (union (A,J2)))) >= (card (Ai \/ (union (A,(J1 \/ J2))))) + (card (union (A,(J1 /\ J2)))) by XREAL_1:7;
J1 c= dom A by A15, Def2;
then A36: J1 \/ J2 c= dom A by A27, XBOOLE_1:8;
A37: i in dom A by A2, CARD_1:27, FUNCT_1:def_2;
then {i} c= dom A by ZFMISC_1:31;
then L c= dom A by A36, XBOOLE_1:8;
then card (union (A,({i} \/ (J1 \/ J2)))) >= card ({i} \/ (J1 \/ J2)) by A1, Def4;
then A38: card (union (A,(({i} \/ J1) \/ J2))) >= card ({i} \/ (J1 \/ J2)) by XBOOLE_1:4;
not i in J1 \/ J2 by A14, A24, XBOOLE_0:def_3;
then A39: card ({i} \/ (J1 \/ J2)) = (card {i}) + (card (J1 \/ J2)) by CARD_2:40, ZFMISC_1:50;
( J1 /\ J2 c= J1 & J1 c= dom A ) by A15, Def2, XBOOLE_1:17;
then J1 /\ J2 c= dom A by XBOOLE_1:1;
then A40: card (union (A,(J1 /\ J2))) >= card (J1 /\ J2) by A1, Def4;
set S2 = (union (A,J2)) \/ ((A . i) \ {y});
set S1 = (union (A,J1)) \/ ((A . i) \ {x});
(card J1) + (card J2) >= (card ((union (A,J1)) \/ ((A . i) \ {x}))) + (card ((union (A,J2)) \/ ((A . i) \ {y}))) by A16, A26, XREAL_1:7;
then A41: (card J1) + (card J2) >= (card (((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y})))) + (card (((union (A,J1)) \/ (Ai \ {x})) /\ ((union (A,J2)) \/ (Ai \ {y})))) by Th1;
(union (A,J1)) /\ (union (A,J2)) c= ((union (A,J1)) \/ (Ai \ {x})) /\ ((union (A,J2)) \/ (Ai \ {y}))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (union (A,J1)) /\ (union (A,J2)) or a in ((union (A,J1)) \/ (Ai \ {x})) /\ ((union (A,J2)) \/ (Ai \ {y})) )
assume A42: a in (union (A,J1)) /\ (union (A,J2)) ; ::_thesis: a in ((union (A,J1)) \/ (Ai \ {x})) /\ ((union (A,J2)) \/ (Ai \ {y}))
then a in union (A,J2) by XBOOLE_0:def_4;
then A43: a in (union (A,J2)) \/ (Ai \ {y}) by XBOOLE_0:def_3;
a in union (A,J1) by A42, XBOOLE_0:def_4;
then a in (union (A,J1)) \/ (Ai \ {x}) by XBOOLE_0:def_3;
hence a in ((union (A,J1)) \/ (Ai \ {x})) /\ ((union (A,J2)) \/ (Ai \ {y})) by A43, XBOOLE_0:def_4; ::_thesis: verum
end;
then card (((union (A,J1)) \/ (Ai \ {x})) /\ ((union (A,J2)) \/ (Ai \ {y}))) >= card ((union (A,J1)) /\ (union (A,J2))) by NAT_1:43;
then (card (((union (A,J1)) \/ (Ai \ {x})) \/ ((union (A,J2)) \/ (Ai \ {y})))) + (card (((union (A,J1)) \/ (Ai \ {x})) /\ ((union (A,J2)) \/ (Ai \ {y})))) >= (card ((union (A,(J1 \/ J2))) \/ Ai)) + (card ((union (A,J1)) /\ (union (A,J2)))) by A31, XREAL_1:7;
then (card J1) + (card J2) >= (card ((union (A,(J1 \/ J2))) \/ Ai)) + (card ((union (A,J1)) /\ (union (A,J2)))) by A41, XXREAL_0:2;
then A44: (card J1) + (card J2) >= (card (Ai \/ (union (A,(J1 \/ J2))))) + (card (union (A,(J1 /\ J2)))) by A35, XXREAL_0:2;
card (union (A,(({i} \/ J1) \/ J2))) = card (Ai \/ (union (A,(J1 \/ J2)))) by A37, Th9;
then card (Ai \/ (union (A,(J1 \/ J2)))) >= 1 + (card (J1 \/ J2)) by A38, A39, CARD_1:30;
then A45: (card (Ai \/ (union (A,(J1 \/ J2))))) + (card (union (A,(J1 /\ J2)))) >= (1 + (card (J1 \/ J2))) + (card (J1 /\ J2)) by A40, XREAL_1:7;
(card (J1 \/ J2)) + (card (J1 /\ J2)) = (card J1) + (card J2) by Th1;
then (1 + (card (J1 \/ J2))) + (card (J1 /\ J2)) = 1 + ((card J1) + (card J2)) ;
hence contradiction by A44, A45, NAT_1:13; ::_thesis: verum
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
let F be finite set ; ::_thesis: 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
let A be FinSequence of bool F; ::_thesis: 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
let i be Element of NAT ; ::_thesis: ( i in dom A & A is Hall implies ex G being Singlification of A,i st G is Hall )
assume that
A1: i in dom A and
A2: A is Hall ; ::_thesis: ex G being Singlification of A,i st G is Hall
A3: A . i <> {} by A1, A2, Th16, CARD_1:27;
set n = card (A . i);
A4: card (A . i) >= 1 by A1, A2, Th16;
defpred S1[ Element of NAT ] means ex G being Reduction of A st
( G is Hall & card (G . i) = $1 );
A5: A is Reduction of A by Th26;
percases ( card (A . i) = 1 or card (A . i) > 1 ) by A4, XXREAL_0:1;
suppose card (A . i) = 1 ; ::_thesis: ex G being Singlification of A,i st G is Hall
then A is Singlification of A,i by A1, A5, Def7, CARD_1:27;
hence ex G being Singlification of A,i st G is Hall by A2; ::_thesis: verum
end;
supposeA6: card (A . i) > 1 ; ::_thesis: ex G being Singlification of A,i st G is Hall
A7: for k being Element of NAT st k >= 1 & S1[k + 1] holds
S1[k]
proof
let k be Element of NAT ; ::_thesis: ( k >= 1 & S1[k + 1] implies S1[k] )
assume that
A8: k >= 1 and
A9: S1[k + 1] ; ::_thesis: S1[k]
consider G being Reduction of A such that
A10: G is Hall and
A11: card (G . i) = k + 1 by A9;
1 + 1 <= k + 1 by A8, XREAL_1:6;
then consider x being set such that
A12: x in G . i and
A13: Cut (G,i,x) is Hall by A10, A11, Th29;
set H = Cut (G,i,x);
A14: dom G = dom A by Def6;
then Cut (G,i,x) is Reduction of G by A1, Th21;
then A15: Cut (G,i,x) is Reduction of A by Th22;
card ((Cut (G,i,x)) . i) = (k + 1) - 1 by A1, A11, A14, A12, Th11
.= k ;
hence S1[k] by A13, A15; ::_thesis: verum
end;
A is Reduction of A by Th26;
then A16: ex n being Element of NAT st
( n > 1 & S1[n] ) by A2, A6;
S1[1] from HALLMAR1:sch_2(A16, A7);
then consider G being Reduction of A such that
A17: G is Hall and
A18: card (G . i) = 1 ;
G is Singlification of A,i by A1, A3, A18, Def7;
hence ex G being Singlification of A,i st G is Hall by A17; ::_thesis: verum
end;
end;
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
let F be non empty finite set ; ::_thesis: for A being non empty FinSequence of bool F st A is Hall holds
ex G being Singlification of A st G is Hall
let A be non empty FinSequence of bool F; ::_thesis: ( A is Hall implies ex G being Singlification of A st G is Hall )
defpred S1[ Element of NAT ] means ( $1 in dom A implies ex g being Singlification of A,$1 st
( g is Hall & ( for k being Element of NAT st 1 <= k & k <= $1 holds
g is Singlification of A,k ) ) );
assume A1: A is Hall ; ::_thesis: ex G being Singlification of A st G is Hall
then A2: A is non-empty ;
A3: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
( k + 1 in dom A implies ex g being Singlification of A,k + 1 st
( g is Hall & ( for l being Element of NAT st 1 <= l & l <= k + 1 holds
g is Singlification of A,l ) ) )
proof
assume A5: k + 1 in dom A ; ::_thesis: ex g being Singlification of A,k + 1 st
( g is Hall & ( for l being Element of NAT st 1 <= l & l <= k + 1 holds
g is Singlification of A,l ) )
percases ( k = 0 or k in dom A ) by A5, TAXONOM1:1;
supposeA6: k = 0 ; ::_thesis: ex g being Singlification of A,k + 1 st
( g is Hall & ( for l being Element of NAT st 1 <= l & l <= k + 1 holds
g is Singlification of A,l ) )
consider g being Singlification of A,k + 1 such that
A7: g is Hall by A1, A5, Th30;
for l being Element of NAT st 1 <= l & l <= k + 1 holds
g is Singlification of A,l by A6, XXREAL_0:1;
hence ex g being Singlification of A,k + 1 st
( g is Hall & ( for l being Element of NAT st 1 <= l & l <= k + 1 holds
g is Singlification of A,l ) ) by A7; ::_thesis: verum
end;
supposeA8: k in dom A ; ::_thesis: ex g being Singlification of A,k + 1 st
( g is Hall & ( for l being Element of NAT st 1 <= l & l <= k + 1 holds
g is Singlification of A,l ) )
then consider g being Singlification of A,k such that
A9: g is Hall and
A10: for l being Element of NAT st 1 <= l & l <= k holds
g is Singlification of A,l by A4;
k + 1 in dom g by A5, Def6;
then consider G being Singlification of g,k + 1 such that
A11: G is Hall by A9, Th30;
A12: dom g = dom A by Def6;
then A13: dom G = dom A by Def6;
then A14: G . k <> {} by A8, A11;
A15: g . (k + 1) <> {} by A9, A5, A12;
then reconsider G = G as Singlification of A,k + 1 by A2, A5, A8, A14, Th24;
for l being Element of NAT st 1 <= l & l <= k + 1 holds
G is Singlification of A,l
proof
let l be Element of NAT ; ::_thesis: ( 1 <= l & l <= k + 1 implies G is Singlification of A,l )
assume that
A16: 1 <= l and
A17: l <= k + 1 ; ::_thesis: G is Singlification of A,l
k + 1 <= len A by A5, FINSEQ_3:25;
then l <= len A by A17, XXREAL_0:2;
then A18: l in dom A by A16, FINSEQ_3:25;
then A19: G . l <> {} by A13, A11;
percases ( l <= k or l = k + 1 ) by A17, NAT_1:8;
suppose l <= k ; ::_thesis: G is Singlification of A,l
then g is Singlification of A,l by A10, A16;
hence G is Singlification of A,l by A2, A5, A15, A18, A19, Th24; ::_thesis: verum
end;
suppose l = k + 1 ; ::_thesis: G is Singlification of A,l
hence G is Singlification of A,l ; ::_thesis: verum
end;
end;
end;
hence ex g being Singlification of A,k + 1 st
( g is Hall & ( for l being Element of NAT st 1 <= l & l <= k + 1 holds
g is Singlification of A,l ) ) by A11; ::_thesis: verum
end;
end;
end;
hence S1[k + 1] ; ::_thesis: verum
end;
A20: S1[ 0 ]
proof
assume 0 in dom A ; ::_thesis: ex g being Singlification of A, 0 st
( g is Hall & ( for k being Element of NAT st 1 <= k & k <= 0 holds
g is Singlification of A,k ) )
then consider G being Singlification of A, 0 such that
A21: G is Hall by A1, Th30;
for k being Element of NAT st 1 <= k & k <= 0 holds
G is Singlification of A,k ;
hence ex g being Singlification of A, 0 st
( g is Hall & ( for k being Element of NAT st 1 <= k & k <= 0 holds
g is Singlification of A,k ) ) by A21; ::_thesis: verum
end;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A20, A3);
then ( len A in dom A implies ex g being Singlification of A, len A st
( g is Hall & ( for l being Element of NAT st 1 <= l & l <= len A holds
g is Singlification of A,l ) ) ) ;
then consider G being Singlification of A, len A such that
A22: G is Hall and
A23: for l being Element of NAT st 1 <= l & l <= len A holds
G is Singlification of A,l by FINSEQ_5:6;
A24: for i being Element of NAT st i in dom A holds
G is Singlification of A,i
proof
let i be Element of NAT ; ::_thesis: ( i in dom A implies G is Singlification of A,i )
assume i in dom A ; ::_thesis: G is Singlification of A,i
then ( 1 <= i & i <= len A ) by FINSEQ_3:25;
hence G is Singlification of A,i by A23; ::_thesis: verum
end;
dom G = dom A by Def6;
then G is Singlification of A by A2, A24, Th27;
hence ex G being Singlification of A st G is Hall by A22; ::_thesis: verum
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
let F be non empty finite set ; ::_thesis: 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 )
let A be non empty FinSequence of bool F; ::_thesis: ( ex X being set st X is_a_system_of_different_representatives_of A iff A is Hall )
thus ( ex X being set st X is_a_system_of_different_representatives_of A implies A is Hall ) by Th18; ::_thesis: ( A is Hall implies ex X being set st X is_a_system_of_different_representatives_of A )
assume A1: A is Hall ; ::_thesis: ex X being set st X is_a_system_of_different_representatives_of A
then consider G being Singlification of A such that
A2: G is Hall by Th31;
for i being Element of NAT st i in dom G holds
card (G . i) = 1
proof
let i be Element of NAT ; ::_thesis: ( i in dom G implies card (G . i) = 1 )
assume A3: i in dom G ; ::_thesis: card (G . i) = 1
dom G = dom A by Def6;
hence card (G . i) = 1 by A1, A3, Def8; ::_thesis: verum
end;
then ex X being set st X is_a_system_of_different_representatives_of G by A2, Th17;
hence ex X being set st X is_a_system_of_different_representatives_of A by Th28; ::_thesis: verum
end;