let T be TopStruct ; 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 ; 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; ( T is compact & f is continuous & rng f = [#] S implies S is compact )
assume A1:
T is compact
; ( not f is continuous or not rng f = [#] S or S is compact )
[#] T c= dom f
by FUNCT_2:def 1;
then A2:
[#] T c= f " (f .: ([#] T))
by FUNCT_1:76;
assume that
A3:
f is continuous
and
A4:
rng f = [#] S
; S is compact
let F be Subset-Family of S; COMPTS_1:def 1 ( 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
A5:
F is Cover of S
and
A6:
F is open
; 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:42;
union G =
f " (union F)
by A4, FUNCT_3:26
.=
f " (rng f)
by A4, A5, SETFAM_1:45
.=
f " (f .: (dom f))
by RELAT_1:113
.=
f " (f .: ([#] T))
by FUNCT_2:def 1
;
then A7:
G is Cover of T
by A2, SETFAM_1:def 11;
A8:
(.: f) .: ((.: f) " F) c= F
by FUNCT_1:75;
(.: f) .: ((" f) .: F) c= (.: f) .: ((.: f) " F)
by FUNCT_3:29, RELAT_1:123;
then A9:
(.: f) .: G c= F
by A8;
G is open
by A3, A6, TOPS_2:47;
then consider G9 being Subset-Family of T such that
A10:
G9 c= G
and
A11:
G9 is Cover of T
and
A12:
G9 is finite
by A1, A7;
reconsider F9 = (.: f) .: G9 as Subset-Family of S ;
take
F9
; ( F9 c= F & F9 is Cover of S & F9 is finite )
(.: f) .: G9 c= (.: f) .: G
by A10, RELAT_1:123;
hence
F9 c= F
by A9; ( F9 is Cover of S & F9 is finite )
dom f = [#] T
by FUNCT_2:def 1;
then union F9 =
f .: (union G9)
by FUNCT_3:14
.=
f .: ([#] T)
by A11, SETFAM_1:45
.=
f .: (dom f)
by FUNCT_2:def 1
.=
[#] S
by A4, RELAT_1:113
;
hence
F9 is Cover of S
by SETFAM_1:def 11; F9 is finite
thus
F9 is finite
by A12; verum