let X be non empty TopSpace; :: thesis: for f being Function of the carrier of X,COMPLEX holds
( f is continuous iff for Y being Subset of COMPLEX st Y is open holds
f " Y is open )
let f be Function of the carrier of X,COMPLEX; :: thesis: ( f is continuous iff for Y being Subset of COMPLEX st Y is open holds
f " Y is open )
hereby :: thesis: ( ( for Y being Subset of COMPLEX st Y is open holds
f " Y is open ) implies f is continuous )
assume A1: f is continuous ; :: thesis: for Y being Subset of COMPLEX st Y is open holds
f " Y is open
let Y be Subset of COMPLEX; :: thesis: ( Y is open implies f " Y is open )
assume Y is open ; :: thesis: f " Y is open
then Y ` is closed by CFDIFF_1:def 11;
then A2: f " (Y `) is closed by A1;
f " (Y `) = (f " COMPLEX) \ (f " Y) by FUNCT_1:69
.= ([#] X) \ (f " Y) by FUNCT_2:40 ;
then ([#] X) \ (([#] X) \ (f " Y)) is open by A2, PRE_TOPC:def 3;
hence f " Y is open by PRE_TOPC:3; :: thesis: verum
end;
assume A3: for Y being Subset of COMPLEX st Y is open holds
f " Y is open ; :: thesis: f is continuous
let Y be Subset of COMPLEX; :: according to CC0SP2:def 1 :: thesis: ( Y is closed implies f " Y is closed )
assume A4: Y is closed ; :: thesis: f " Y is closed
Y = (Y `) ` ;
then Y ` is open by A4, CFDIFF_1:def 11;
then A5: f " (Y `) is open by A3;
f " (Y `) = (f " COMPLEX) \ (f " Y) by FUNCT_1:69
.= ([#] X) \ (f " Y) by FUNCT_2:40 ;
hence f " Y is closed by A5, PRE_TOPC:def 3; :: thesis: verum