let T be TopStruct ; :: thesis: for f being RealMap of T holds
( f is continuous iff for Y being Subset of REAL st Y is open holds
f " Y is open )
let f be RealMap of T; :: thesis: ( f is continuous iff for Y being Subset of REAL st Y is open holds
f " Y is open )
hereby :: thesis: ( ( for Y being Subset of REAL st Y is open holds
f " Y is open ) implies f is continuous )
assume A1: f is continuous ; :: thesis: for Y being Subset of REAL st Y is open holds
f " Y is open
let Y be Subset of REAL; :: thesis: ( Y is open implies f " Y is open )
assume Y is open ; :: thesis: f " Y is open
then Y ` is closed ;
then A2: f " (Y `) is closed by A1;
f " (Y `) = (f " REAL) \ (f " Y) by FUNCT_1:69
.= ([#] T) \ (f " Y) by FUNCT_2:40 ;
then ([#] T) \ (([#] T) \ (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 REAL st Y is open holds
f " Y is open ; :: thesis: f is continuous
let Y be Subset of REAL; :: according to PSCOMP_1:def 3 :: thesis: ( Y is closed implies f " Y is closed )
assume Y is closed ; :: thesis: f " Y is closed
then Y ` is open ;
then A4: f " (Y `) is open by A3;
f " (Y `) = (f " REAL) \ (f " Y) by FUNCT_1:69
.= ([#] T) \ (f " Y) by FUNCT_2:40 ;
hence f " Y is closed by A4, PRE_TOPC:def 3; :: thesis: verum