let T be TopSpace; :: thesis: for S being non empty TopSpace
for f being Function of T,S holds
( f is continuous iff for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) )
let S be non empty TopSpace; :: thesis: for f being Function of T,S holds
( f is continuous iff for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) )
let f be Function of T,S; :: thesis: ( f is continuous iff for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) )
hereby :: thesis: ( ( for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) ) implies f is continuous )
assume A1: f is continuous ; :: thesis: for P being Subset of T holds f .: (Cl P) c= Cl (f .: P)
let P be Subset of T; :: thesis: f .: (Cl P) c= Cl (f .: P)
P c= [#] T ;
then P c= dom f by FUNCT_2:def 1;
then A2: Cl P c= Cl (f " (f .: P)) by FUNCT_1:76, PRE_TOPC:19;
Cl (f " (f .: P)) c= f " (Cl (f .: P)) by A1, Th44;
then Cl P c= f " (Cl (f .: P)) by A2;
then A3: f .: (Cl P) c= f .: (f " (Cl (f .: P))) by RELAT_1:123;
f .: (f " (Cl (f .: P))) c= Cl (f .: P) by FUNCT_1:75;
hence f .: (Cl P) c= Cl (f .: P) by A3; :: thesis: verum
end;
assume A4: for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) ; :: thesis: f is continuous
now :: thesis: for P1 being Subset of S holds Cl (f " P1) c= f " (Cl P1)
let P1 be Subset of S; :: thesis: Cl (f " P1) c= f " (Cl P1)
Cl (f " P1) c= [#] T ;
then Cl (f " P1) c= dom f by FUNCT_2:def 1;
then A5: Cl (f " P1) c= f " (f .: (Cl (f " P1))) by FUNCT_1:76;
( f .: (Cl (f " P1)) c= Cl (f .: (f " P1)) & Cl (f .: (f " P1)) c= Cl P1 ) by A4, FUNCT_1:75, PRE_TOPC:19;
then f .: (Cl (f " P1)) c= Cl P1 ;
then f " (f .: (Cl (f " P1))) c= f " (Cl P1) by RELAT_1:143;
hence Cl (f " P1) c= f " (Cl P1) by A5; :: thesis: verum
end;
hence f is continuous by Th44; :: thesis: verum