let X, Y be RealNormSpace; :: thesis: for f being PartFunc of X,Y

for A being Subset of X

for B being Subset of Y st dom f = A & f is_continuous_on A & A is open & B is open holds

f " B is open

let f be PartFunc of X,Y; :: thesis: for A being Subset of X

for B being Subset of Y st dom f = A & f is_continuous_on A & A is open & B is open holds

f " B is open

let A be Subset of X; :: thesis: for B being Subset of Y st dom f = A & f is_continuous_on A & A is open & B is open holds

f " B is open

let B be Subset of Y; :: thesis: ( dom f = A & f is_continuous_on A & A is open & B is open implies f " B is open )

assume that

A1: dom f = A and

A2: f is_continuous_on A and

A3: A is open and

A4: B is open ; :: thesis: f " B is open

for a being Point of X st a in f " B holds

ex s being Real st

( s > 0 & Ball (a,s) c= f " B )

for A being Subset of X

for B being Subset of Y st dom f = A & f is_continuous_on A & A is open & B is open holds

f " B is open

let f be PartFunc of X,Y; :: thesis: for A being Subset of X

for B being Subset of Y st dom f = A & f is_continuous_on A & A is open & B is open holds

f " B is open

let A be Subset of X; :: thesis: for B being Subset of Y st dom f = A & f is_continuous_on A & A is open & B is open holds

f " B is open

let B be Subset of Y; :: thesis: ( dom f = A & f is_continuous_on A & A is open & B is open implies f " B is open )

assume that

A1: dom f = A and

A2: f is_continuous_on A and

A3: A is open and

A4: B is open ; :: thesis: f " B is open

for a being Point of X st a in f " B holds

ex s being Real st

( s > 0 & Ball (a,s) c= f " B )

proof

hence
f " B is open
by NDIFF_8:20; :: thesis: verum
let a be Point of X; :: thesis: ( a in f " B implies ex s being Real st

( s > 0 & Ball (a,s) c= f " B ) )

assume a in f " B ; :: thesis: ex s being Real st

( s > 0 & Ball (a,s) c= f " B )

then A6: ( a in dom f & f . a in B ) by FUNCT_1:def 7;

then f /. a in B by PARTFUN1:def 6;

then consider t being Real such that

A7: ( t > 0 & Ball ((f /. a),t) c= B ) by A4, NDIFF_8:20;

consider s0 being Real such that

A8: ( 0 < s0 & ( for a1 being Point of X st a1 in A & ||.(a1 - a).|| < s0 holds

||.((f /. a1) - (f /. a)).|| < t ) ) by A1, A2, A6, A7, NFCONT_1:19;

consider s1 being Real such that

A9: ( 0 < s1 & Ball (a,s1) c= A ) by A1, A3, A6, NDIFF_8:20;

set s = min (s0,s1);

A10: min (s0,s1) <= s0 by XXREAL_0:17;

A11: min (s0,s1) <= s1 by XXREAL_0:17;

take min (s0,s1) ; :: thesis: ( min (s0,s1) > 0 & Ball (a,(min (s0,s1))) c= f " B )

thus 0 < min (s0,s1) by A8, A9, XXREAL_0:15; :: thesis: Ball (a,(min (s0,s1))) c= f " B

for a1 being object st a1 in Ball (a,(min (s0,s1))) holds

a1 in f " B

end;( s > 0 & Ball (a,s) c= f " B ) )

assume a in f " B ; :: thesis: ex s being Real st

( s > 0 & Ball (a,s) c= f " B )

then A6: ( a in dom f & f . a in B ) by FUNCT_1:def 7;

then f /. a in B by PARTFUN1:def 6;

then consider t being Real such that

A7: ( t > 0 & Ball ((f /. a),t) c= B ) by A4, NDIFF_8:20;

consider s0 being Real such that

A8: ( 0 < s0 & ( for a1 being Point of X st a1 in A & ||.(a1 - a).|| < s0 holds

||.((f /. a1) - (f /. a)).|| < t ) ) by A1, A2, A6, A7, NFCONT_1:19;

consider s1 being Real such that

A9: ( 0 < s1 & Ball (a,s1) c= A ) by A1, A3, A6, NDIFF_8:20;

set s = min (s0,s1);

A10: min (s0,s1) <= s0 by XXREAL_0:17;

A11: min (s0,s1) <= s1 by XXREAL_0:17;

take min (s0,s1) ; :: thesis: ( min (s0,s1) > 0 & Ball (a,(min (s0,s1))) c= f " B )

thus 0 < min (s0,s1) by A8, A9, XXREAL_0:15; :: thesis: Ball (a,(min (s0,s1))) c= f " B

for a1 being object st a1 in Ball (a,(min (s0,s1))) holds

a1 in f " B

proof

hence
Ball (a,(min (s0,s1))) c= f " B
by TARSKI:def 3; :: thesis: verum
let a1 be object ; :: thesis: ( a1 in Ball (a,(min (s0,s1))) implies a1 in f " B )

assume A13: a1 in Ball (a,(min (s0,s1))) ; :: thesis: a1 in f " B

then reconsider a1 = a1 as Point of X ;

A14: a1 in Ball (a,s1) by A11, A13, NDIFF_8:15, TARSKI:def 3;

A15: a1 in Ball (a,s0) by A10, A13, NDIFF_8:15, TARSKI:def 3;

a1 in { x where x is Point of X : ||.(x - a).|| < s0 } by A15, NDIFF_8:17;

then ex x being Point of X st

( a1 = x & ||.(x - a).|| < s0 ) ;

then ||.((f /. a1) - (f /. a)).|| < t by A8, A9, A14;

then f /. a1 in { y where y is Point of Y : ||.(y - (f /. a)).|| < t } ;

then f /. a1 in Ball ((f /. a),t) by NDIFF_8:17;

then f . a1 in Ball ((f /. a),t) by A1, A9, A14, PARTFUN1:def 6;

hence a1 in f " B by A1, A7, A9, A14, FUNCT_1:def 7; :: thesis: verum

end;assume A13: a1 in Ball (a,(min (s0,s1))) ; :: thesis: a1 in f " B

then reconsider a1 = a1 as Point of X ;

A14: a1 in Ball (a,s1) by A11, A13, NDIFF_8:15, TARSKI:def 3;

A15: a1 in Ball (a,s0) by A10, A13, NDIFF_8:15, TARSKI:def 3;

a1 in { x where x is Point of X : ||.(x - a).|| < s0 } by A15, NDIFF_8:17;

then ex x being Point of X st

( a1 = x & ||.(x - a).|| < s0 ) ;

then ||.((f /. a1) - (f /. a)).|| < t by A8, A9, A14;

then f /. a1 in { y where y is Point of Y : ||.(y - (f /. a)).|| < t } ;

then f /. a1 in Ball ((f /. a),t) by NDIFF_8:17;

then f . a1 in Ball ((f /. a),t) by A1, A9, A14, PARTFUN1:def 6;

hence a1 in f " B by A1, A7, A9, A14, FUNCT_1:def 7; :: thesis: verum