let X, Y be non empty compact TopSpace; for R being Subset-Family of X
for F being Subset-Family of [:Y,X:] st F is Cover of [:Y,X:] & F is open & 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 ) } holds
( R is open & R is Cover of X )
let R be Subset-Family of X; for F being Subset-Family of [:Y,X:] st F is Cover of [:Y,X:] & F is open & 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 ) } holds
( R is open & R is Cover of X )
let F be Subset-Family of [:Y,X:]; ( F is Cover of [:Y,X:] & F is open & 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 ) } implies ( R is open & R is Cover of X ) )
assume that
A1:
F is Cover of [:Y,X:]
and
A2:
F is open
and
A3:
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 ) }
; ( R is open & R is Cover of X )
hence
R is open
; R is Cover of X
A4:
union F = [#] [:Y,X:]
by A1, SETFAM_1:45;
[#] X c= union R
proof
let k be
object ;
TARSKI:def 3 ( not k in [#] X or k in union R )
assume
k in [#] X
;
k in union R
then reconsider k9 =
k as
Point of
X ;
reconsider Z =
[:([#] Y),{k9}:] as
Subset of
[:Y,X:] ;
(
F is
Cover of
Z &
Z is
compact )
by A4, Th16, SETFAM_1:def 11;
then consider G being
Subset-Family of
[:Y,X:] such that A5:
G c= F
and A6:
G is
Cover of
Z
and A7:
G is
finite
by A2;
set uR =
union G;
set Q =
{ x where x is Point of X : [:([#] Y),{x}:] c= union G } ;
{ x where x is Point of X : [:([#] Y),{x}:] c= union G } c= the
carrier of
X
then reconsider Q =
{ x where x is Point of X : [:([#] Y),{x}:] c= union G } as
Subset of
X ;
Z c= union G
by A6, SETFAM_1:def 11;
then A8:
k9 in Q
;
A9:
ex
FQ being
Subset-Family of
[:Y,X:] st
(
FQ c= F &
FQ is
finite &
[:([#] Y),Q:] c= union FQ )
union G is
open
by A2, A5, TOPS_2:11, TOPS_2:19;
then
Q in the
topology of
X
by Th12;
then
Q is
open
by PRE_TOPC:def 2;
then
Q in R
by A3, A9;
hence
k in union R
by A8, TARSKI:def 4;
verum
end;
hence
R is Cover of X
by SETFAM_1:def 11; verum