let X, Y be non empty compact TopSpace; for F being Subset-Family of [:Y,X:] st F is Cover of [:Y,X:] & F is open holds
ex G being Subset-Family of [:Y,X:] st
( G c= F & G is Cover of [:Y,X:] & G is finite )
let F be Subset-Family of [:Y,X:]; ( F is Cover of [:Y,X:] & F is open implies ex G being Subset-Family of [:Y,X:] st
( G c= F & G is Cover of [:Y,X:] & G is finite ) )
set R = { Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ ) } ;
{ Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ ) } c= bool the carrier of X
then reconsider R = { Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ ) } as Subset-Family of X ;
reconsider R = R as Subset-Family of X ;
defpred S1[ object , object ] means ex D1 being set ex FQ being Subset-Family of [:Y,X:] st
( D1 = $1 & FQ c= F & FQ is finite & [:([#] Y),D1:] c= union FQ & $2 = FQ );
deffunc H1( set ) -> set = [:([#] Y),$1:];
assume
( F is Cover of [:Y,X:] & F is open )
; ex G being Subset-Family of [:Y,X:] st
( G c= F & G is Cover of [:Y,X:] & G is finite )
then consider C being Subset-Family of X such that
A1:
C c= R
and
A2:
C is finite
and
A3:
C is Cover of X
by Th19;
set CX = { H1(f) where f is Subset of X : f in C } ;
{ H1(f) where f is Subset of X : f in C } c= bool the carrier of [:Y,X:]
then reconsider CX = { H1(f) where f is Subset of X : f in C } as Subset-Family of [:Y,X:] ;
reconsider CX = CX as Subset-Family of [:Y,X:] ;
A5:
for e being object st e in C holds
ex u being object st S1[e,u]
consider t being Function such that
A6:
( dom t = C & ( for s being object st s in C holds
S1[s,t . s] ) )
from CLASSES1:sch 1(A5);
set G = union (rng t);
A7:
union (rng t) c= F
union (rng t) c= bool the carrier of [:Y,X:]
then reconsider G = union (rng t) as Subset-Family of [:Y,X:] ;
reconsider G = G as Subset-Family of [:Y,X:] ;
take
G
; ( G c= F & G is Cover of [:Y,X:] & G is finite )
thus
G c= F
by A7; ( G is Cover of [:Y,X:] & G is finite )
union CX = [:([#] Y),(union C):]
proof
hereby TARSKI:def 3,
XBOOLE_0:def 10 [:([#] Y),(union C):] c= union CX
let g be
object ;
( g in union CX implies g in [:([#] Y),(union C):] )assume
g in union CX
;
g in [:([#] Y),(union C):]then consider GG being
set such that A11:
g in GG
and A12:
GG in CX
by TARSKI:def 4;
consider FF being
Subset of
X such that A13:
GG = [:([#] Y),FF:]
and A14:
FF in C
by A12;
consider g1,
g2 being
object such that A15:
g1 in [#] Y
and A16:
g2 in FF
and A17:
g = [g1,g2]
by A11, A13, ZFMISC_1:def 2;
g2 in union C
by A14, A16, TARSKI:def 4;
hence
g in [:([#] Y),(union C):]
by A15, A17, ZFMISC_1:87;
verum
end;
let g be
object ;
TARSKI:def 3 ( not g in [:([#] Y),(union C):] or g in union CX )
assume
g in [:([#] Y),(union C):]
;
g in union CX
then consider g1,
g2 being
object such that A18:
g1 in [#] Y
and A19:
g2 in union C
and A20:
g = [g1,g2]
by ZFMISC_1:def 2;
consider GG being
set such that A21:
g2 in GG
and A22:
GG in C
by A19, TARSKI:def 4;
GG in { Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ ) }
by A1, A22;
then consider Q1 being
open Subset of
X such that A23:
GG = Q1
and
ex
FQ being
Subset-Family of
[:Y,X:] st
(
FQ c= F &
FQ is
finite &
[:([#] Y),Q1:] c= union FQ )
;
A24:
[:([#] Y),Q1:] in CX
by A22, A23;
g in [:([#] Y),Q1:]
by A18, A20, A21, A23, ZFMISC_1:87;
hence
g in union CX
by A24, TARSKI:def 4;
verum
end;
then A25: union CX =
[:([#] Y),([#] X):]
by A3, SETFAM_1:45
.=
[#] [:Y,X:]
by BORSUK_1:def 2
;
[#] [:Y,X:] c= union (union (rng t))
proof
let d be
object ;
TARSKI:def 3 ( not d in [#] [:Y,X:] or d in union (union (rng t)) )
assume
d in [#] [:Y,X:]
;
d in union (union (rng t))
then consider CC being
set such that A26:
d in CC
and A27:
CC in CX
by A25, TARSKI:def 4;
consider Cc being
Subset of
X such that A28:
CC = [:([#] Y),Cc:]
and A29:
Cc in C
by A27;
Cc in R
by A1, A29;
then consider Qq being
open Subset of
X such that A30:
Cc = Qq
and
ex
FQ being
Subset-Family of
[:Y,X:] st
(
FQ c= F &
FQ is
finite &
[:([#] Y),Qq:] c= union FQ )
;
S1[
Cc,
t . Cc]
by A6, A29;
then consider FQ1 being
Subset-Family of
[:Y,X:] such that
FQ1 c= F
and
FQ1 is
finite
and A31:
[:([#] Y),Qq:] c= union FQ1
and A32:
t . Qq = FQ1
by A30;
consider DC being
set such that A33:
d in DC
and A34:
DC in FQ1
by A26, A28, A30, A31, TARSKI:def 4;
FQ1 in rng t
by A6, A29, A30, A32, FUNCT_1:def 3;
then
DC in union (rng t)
by A34, TARSKI:def 4;
hence
d in union (union (rng t))
by A33, TARSKI:def 4;
verum
end;
hence
G is Cover of [:Y,X:]
by SETFAM_1:def 11; G is finite
A35:
for X1 being set st X1 in rng t holds
X1 is finite
rng t is finite
by A2, A6, FINSET_1:8;
hence
G is finite
by A35, FINSET_1:7; verum