let X, Y be RealNormSpace; 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; 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; 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; ( 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
; 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
let a be
Point of
X;
( a in f " B implies ex s being Real st
( s > 0 & Ball (a,s) c= f " B ) )
assume
a in f " B
;
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)
;
( min (s0,s1) > 0 & Ball (a,(min (s0,s1))) c= f " B )
thus
0 < min (
s0,
s1)
by A8, A9, XXREAL_0:15;
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
let a1 be
object ;
( a1 in Ball (a,(min (s0,s1))) implies a1 in f " B )
assume A13:
a1 in Ball (
a,
(min (s0,s1)))
;
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;
verum
end;
hence
Ball (
a,
(min (s0,s1)))
c= f " B
by TARSKI:def 3;
verum
end;
hence
f " B is open
by NDIFF_8:20; verum