let X, Y be non empty TopSpace; :: thesis: for f being Function of X,Y holds

( f is open iff for p being Point of X

for V being open Subset of X st p in V holds

ex W being open Subset of Y st

( f . p in W & W c= f .: V ) )

let f be Function of X,Y; :: thesis: ( f is open iff for p being Point of X

for V being open Subset of X st p in V holds

ex W being open Subset of Y st

( f . p in W & W c= f .: V ) )

thus ( f is open implies for p being Point of X

for V being open Subset of X st p in V holds

ex W being open Subset of Y st

( f . p in W & W c= f .: V ) ) :: thesis: ( ( for p being Point of X

for V being open Subset of X st p in V holds

ex W being open Subset of Y st

( f . p in W & W c= f .: V ) ) implies f is open )

for V being open Subset of X st p in V holds

ex W being open Subset of Y st

( f . p in W & W c= f .: V ) ; :: thesis: f is open

for p being Point of X

for P being open a_neighborhood of p ex R being a_neighborhood of f . p st R c= f .: P

( f is open iff for p being Point of X

for V being open Subset of X st p in V holds

ex W being open Subset of Y st

( f . p in W & W c= f .: V ) )

let f be Function of X,Y; :: thesis: ( f is open iff for p being Point of X

for V being open Subset of X st p in V holds

ex W being open Subset of Y st

( f . p in W & W c= f .: V ) )

thus ( f is open implies for p being Point of X

for V being open Subset of X st p in V holds

ex W being open Subset of Y st

( f . p in W & W c= f .: V ) ) :: thesis: ( ( for p being Point of X

for V being open Subset of X st p in V holds

ex W being open Subset of Y st

( f . p in W & W c= f .: V ) ) implies f is open )

proof

assume A4:
for p being Point of X
assume A1:
f is open
; :: thesis: for p being Point of X

for V being open Subset of X st p in V holds

ex W being open Subset of Y st

( f . p in W & W c= f .: V )

let p be Point of X; :: thesis: for V being open Subset of X st p in V holds

ex W being open Subset of Y st

( f . p in W & W c= f .: V )

let V be open Subset of X; :: thesis: ( p in V implies ex W being open Subset of Y st

( f . p in W & W c= f .: V ) )

assume A2: p in V ; :: thesis: ex W being open Subset of Y st

( f . p in W & W c= f .: V )

V is a_neighborhood of p by A2, CONNSP_2:3;

then consider W being open a_neighborhood of f . p such that

A3: W c= f .: V by A1, TOPGRP_1:22;

take W ; :: thesis: ( f . p in W & W c= f .: V )

thus f . p in W by CONNSP_2:4; :: thesis: W c= f .: V

thus W c= f .: V by A3; :: thesis: verum

end;for V being open Subset of X st p in V holds

ex W being open Subset of Y st

( f . p in W & W c= f .: V )

let p be Point of X; :: thesis: for V being open Subset of X st p in V holds

ex W being open Subset of Y st

( f . p in W & W c= f .: V )

let V be open Subset of X; :: thesis: ( p in V implies ex W being open Subset of Y st

( f . p in W & W c= f .: V ) )

assume A2: p in V ; :: thesis: ex W being open Subset of Y st

( f . p in W & W c= f .: V )

V is a_neighborhood of p by A2, CONNSP_2:3;

then consider W being open a_neighborhood of f . p such that

A3: W c= f .: V by A1, TOPGRP_1:22;

take W ; :: thesis: ( f . p in W & W c= f .: V )

thus f . p in W by CONNSP_2:4; :: thesis: W c= f .: V

thus W c= f .: V by A3; :: thesis: verum

for V being open Subset of X st p in V holds

ex W being open Subset of Y st

( f . p in W & W c= f .: V ) ; :: thesis: f is open

for p being Point of X

for P being open a_neighborhood of p ex R being a_neighborhood of f . p st R c= f .: P

proof

hence
f is open
by TOPGRP_1:23; :: thesis: verum
let p be Point of X; :: thesis: for P being open a_neighborhood of p ex R being a_neighborhood of f . p st R c= f .: P

let P be open a_neighborhood of p; :: thesis: ex R being a_neighborhood of f . p st R c= f .: P

consider W being open Subset of Y such that

A5: f . p in W and

A6: W c= f .: P by A4, CONNSP_2:4;

W is a_neighborhood of f . p by A5, CONNSP_2:3;

hence ex R being a_neighborhood of f . p st R c= f .: P by A6; :: thesis: verum

end;let P be open a_neighborhood of p; :: thesis: ex R being a_neighborhood of f . p st R c= f .: P

consider W being open Subset of Y such that

A5: f . p in W and

A6: W c= f .: P by A4, CONNSP_2:4;

W is a_neighborhood of f . p by A5, CONNSP_2:3;

hence ex R being a_neighborhood of f . p st R c= f .: P by A6; :: thesis: verum