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