let T be TopStruct ; :: thesis: for S being non empty TopStruct
for f being Function of T,S st T is compact & f is continuous & rng f = [#] S holds
S is compact
let S be non empty TopStruct ; :: thesis: for f being Function of T,S st T is compact & f is continuous & rng f = [#] S holds
S is compact
let f be Function of T,S; :: thesis: ( T is compact & f is continuous & rng f = [#] S implies S is compact )
assume A1: T is compact ; :: thesis: ( not f is continuous or not rng f = [#] S or S is compact )
assume that
A2: f is continuous and
A3: rng f = [#] S ; :: thesis: S is compact
let F be Subset-Family of S; :: according to COMPTS_1:def 3 :: thesis: ( F is Cover of S & F is open implies ex G being Subset-Family of S st
( G c= F & G is Cover of S & G is finite ) )
assume that
A4: F is Cover of S and
A5: F is open ; :: thesis: ex G being Subset-Family of S st
( G c= F & G is Cover of S & G is finite )
set F1 = F;
reconsider G = (" f) .: F as Subset-Family of T by TOPS_2:54;
A6: union G = f " (union F) by A3, FUNCT_3:30
.= f " (rng f) by A3, A4, SETFAM_1:60
.= f " (f .: (dom f)) by RELAT_1:146
.= f " (f .: ([#] T)) by FUNCT_2:def 1 ;
[#] T c= dom f by FUNCT_2:def 1;
then ( [#] T c= f " (f .: ([#] T)) & f " (f .: ([#] T)) c= [#] T ) by FUNCT_1:146;
then A7: G is Cover of T by A6, SETFAM_1:def 12;
G is open by A2, A5, TOPS_2:59;
then consider G' being Subset-Family of T such that
A8: G' c= G and
A9: G' is Cover of T and
A10: G' is finite by A1, A7, Def3;
reconsider F' = (.: f) .: G' as Subset-Family of S ;
take F' ; :: thesis: ( F' c= F & F' is Cover of S & F' is finite )
A11: (.: f) .: G' c= (.: f) .: G by A8, RELAT_1:156;
(" f) .: F c= (.: f) " F by FUNCT_3:33;
then ( (.: f) .: ((" f) .: F) c= (.: f) .: ((.: f) " F) & (.: f) .: ((.: f) " F) c= F ) by FUNCT_1:145, RELAT_1:156;
then (.: f) .: G c= F by XBOOLE_1:1;
hence F' c= F by A11, XBOOLE_1:1; :: thesis: ( F' is Cover of S & F' is finite )
dom f = [#] T by FUNCT_2:def 1;
then union F' = f .: (union G') by FUNCT_3:16
.= f .: ([#] T) by A9, SETFAM_1:60
.= f .: (dom f) by FUNCT_2:def 1
.= [#] S by A3, RELAT_1:146 ;
hence F' is Cover of S by SETFAM_1:def 12; :: thesis: F' is finite
thus F' is finite by A10; :: thesis: verum