let r be Real; :: thesis: for S being RealNormSpace
for E being Subset of S
for f being PartFunc of S,RNS_Real st f is_continuous_on E & dom f = E holds
ex H being Subset of S st
( H /\ E = f " ].-infty,r.[ & H is open )
let S be RealNormSpace; :: thesis: for E being Subset of S
for f being PartFunc of S,RNS_Real st f is_continuous_on E & dom f = E holds
ex H being Subset of S st
( H /\ E = f " ].-infty,r.[ & H is open )
let E be Subset of S; :: thesis: for f being PartFunc of S,RNS_Real st f is_continuous_on E & dom f = E holds
ex H being Subset of S st
( H /\ E = f " ].-infty,r.[ & H is open )
let f be PartFunc of S,RNS_Real; :: thesis: ( f is_continuous_on E & dom f = E implies ex H being Subset of S st
( H /\ E = f " ].-infty,r.[ & H is open ) )
assume that
A1: f is_continuous_on E and
A2: dom f = E ; :: thesis: ex H being Subset of S st
( H /\ E = f " ].-infty,r.[ & H is open )
A3: now :: thesis: for z being object st z in f " ].-infty,r.[ holds
ex t being Point of S st
( t = z & ex s being Real st
( 0 < s & ( for t1 being object st t1 in E /\ { t1 where t1 is Point of S : ||.(t1 - t).|| < s } holds
f . t1 in ].-infty,r.[ ) ) )
let z be object ; :: thesis: ( z in f " ].-infty,r.[ implies ex t being Point of S st
( t = z & ex s being Real st
( 0 < s & ( for t1 being object st t1 in E /\ { t1 where t1 is Point of S : ||.(t1 - t).|| < s } holds
f . t1 in ].-infty,r.[ ) ) ) )
assume A4: z in f " ].-infty,r.[ ; :: thesis: ex t being Point of S st
( t = z & ex s being Real st
( 0 < s & ( for t1 being object st t1 in E /\ { t1 where t1 is Point of S : ||.(t1 - t).|| < s } holds
f . t1 in ].-infty,r.[ ) ) )
then A5: ( z in dom f & f . z in ].-infty,r.[ ) by FUNCT_1:def 7;
then A6: ex t being Real st
( t = f . z & -infty < t & t < r ) ;
reconsider t = z as Point of S by A4;
take t = t; :: thesis: ( t = z & ex s being Real st
( 0 < s & ( for t1 being object st t1 in E /\ { t1 where t1 is Point of S : ||.(t1 - t).|| < s } holds
f . t1 in ].-infty,r.[ ) ) )
thus t = z ; :: thesis: ex s being Real st
( 0 < s & ( for t1 being object st t1 in E /\ { t1 where t1 is Point of S : ||.(t1 - t).|| < s } holds
f . t1 in ].-infty,r.[ ) )
reconsider y = f . t as Real ;
set e = r - y;
consider s being Real such that
A7: ( 0 < s & ( for t1 being Point of S st t1 in E & ||.(t1 - t).|| < s holds
||.((f /. t1) - (f /. t)).|| < r - y ) ) by A2, A5, A6, A1, NFCONT_1:19, XREAL_1:50;
take s = s; :: thesis: ( 0 < s & ( for t1 being object st t1 in E /\ { t1 where t1 is Point of S : ||.(t1 - t).|| < s } holds
f . t1 in ].-infty,r.[ ) )
thus 0 < s by A7; :: thesis: for t1 being object st t1 in E /\ { t1 where t1 is Point of S : ||.(t1 - t).|| < s } holds
f . t1 in ].-infty,r.[
thus for t1 being object st t1 in E /\ { t1 where t1 is Point of S : ||.(t1 - t).|| < s } holds
f . t1 in ].-infty,r.[ :: thesis: verum
proof
let t1 be object ; :: thesis: ( t1 in E /\ { t1 where t1 is Point of S : ||.(t1 - t).|| < s } implies f . t1 in ].-infty,r.[ )
assume A8: t1 in E /\ { t1 where t1 is Point of S : ||.(t1 - t).|| < s } ; :: thesis: f . t1 in ].-infty,r.[
then A9: ( t1 in E & t1 in { t1 where t1 is Point of S : ||.(t1 - t).|| < s } ) by XBOOLE_0:def 4;
reconsider y0 = t1 as Point of S by A8;
A10: ex y1 being Point of S st
( y0 = y1 & ||.(y1 - t).|| < s ) by A9;
reconsider r1 = f /. y0, r2 = f /. t as Real ;
A11: r2 = f . t by A5, PARTFUN1:def 6;
(f /. y0) - (f /. t) = r1 - r2 by DUALSP03:4;
then ||.((f /. y0) - (f /. t)).|| = |.(r1 - r2).| by EUCLID:def 2;
then r1 in ].(r2 - (r - y)),(r2 + (r - y)).[ by A7, A9, A10, RCOMP_1:1;
then ex g being Real st
( g = r1 & r2 - (r - y) < g & g < r2 + (r - y) ) ;
then ( -infty < r1 & r1 < r ) by A11, XXREAL_0:12;
then r1 in ].-infty,r.[ ;
hence f . t1 in ].-infty,r.[ by A9, A1, PARTFUN1:def 6; :: thesis: verum
end;
end;
defpred S1[ object , object ] means ex t being Point of S ex s being Real st
( t = $1 & s = $2 & 0 < s & ( for t1 being object st t1 in E /\ { t1 where t1 is Point of S : ||.(t1 - t).|| < s } holds
f . t1 in ].-infty,r.[ ) );
A12: for z being object st z in f " ].-infty,r.[ holds
ex y being object st
( y in REAL & S1[z,y] )
proof
let z be object ; :: thesis: ( z in f " ].-infty,r.[ implies ex y being object st
( y in REAL & S1[z,y] ) )
assume z in f " ].-infty,r.[ ; :: thesis: ex y being object st
( y in REAL & S1[z,y] )
then consider t being Point of S such that
A13: ( t = z & ex s being Real st
( 0 < s & ( for t1 being object st t1 in E /\ { t1 where t1 is Point of S : ||.(t1 - t).|| < s } holds
f . t1 in ].-infty,r.[ ) ) ) by A3;
consider s being Real such that
A14: ( 0 < s & ( for t1 being object st t1 in E /\ { t1 where t1 is Point of S : ||.(t1 - t).|| < s } holds
f . t1 in ].-infty,r.[ ) ) by A13;
reconsider y = s as Element of REAL by XREAL_0:def 1;
take y ; :: thesis: ( y in REAL & S1[z,y] )
thus y in REAL ; :: thesis: S1[z,y]
thus S1[z,y] by A13, A14; :: thesis: verum
end;
consider R being Function of (f " ].-infty,r.[),REAL such that
A15: for x being object st x in f " ].-infty,r.[ holds
S1[x,R . x] from FUNCT_2:sch 1(A12);
 defpred S2[ object , object ] means ex t being Point of S st
( t = $1 & 0 < R . $1 & $2 = { t1 where t1 is Point of S : ||.(t1 - t).|| < R . $1 } );
A16: for z being object st z in f " ].-infty,r.[ holds
ex y being object st
( y in bool the carrier of S & S2[z,y] )
proof
let z be object ; :: thesis: ( z in f " ].-infty,r.[ implies ex y being object st
( y in bool the carrier of S & S2[z,y] ) )
assume z in f " ].-infty,r.[ ; :: thesis: ex y being object st
( y in bool the carrier of S & S2[z,y] )
then consider t being Point of S, s being Real such that
A17: ( t = z & s = R . z & 0 < s & ( for t1 being object st t1 in E /\ { t1 where t1 is Point of S : ||.(t1 - t).|| < s } holds
f . t1 in ].-infty,r.[ ) ) by A15;
set y = { t1 where t1 is Point of S : ||.(t1 - t).|| < s } ;
take { t1 where t1 is Point of S : ||.(t1 - t).|| < s } ; :: thesis: ( { t1 where t1 is Point of S : ||.(t1 - t).|| < s } in bool the carrier of S & S2[z, { t1 where t1 is Point of S : ||.(t1 - t).|| < s } ] )
now :: thesis: for x being object st x in { t1 where t1 is Point of S : ||.(t1 - t).|| < s } holds
x in the carrier of S
let x be object ; :: thesis: ( x in { t1 where t1 is Point of S : ||.(t1 - t).|| < s } implies x in the carrier of S )
assume x in { t1 where t1 is Point of S : ||.(t1 - t).|| < s } ; :: thesis: x in the carrier of S
then ex t1 being Point of S st
( x = t1 & ||.(t1 - t).|| < s ) ;
hence x in the carrier of S ; :: thesis: verum
end;
then { t1 where t1 is Point of S : ||.(t1 - t).|| < s } c= the carrier of S ;
hence ( { t1 where t1 is Point of S : ||.(t1 - t).|| < s } in bool the carrier of S & S2[z, { t1 where t1 is Point of S : ||.(t1 - t).|| < s } ] ) by A17; :: thesis: verum
end;
consider B being Function of (f " ].-infty,r.[),(bool the carrier of S) such that
A18: for x being object st x in f " ].-infty,r.[ holds
S2[x,B . x] from FUNCT_2:sch 1(A16);
 set H = union (rng B);
reconsider H = union (rng B) as Subset of S ;
take H ; :: thesis: ( H /\ E = f " ].-infty,r.[ & H is open )
for z being object holds
( z in H /\ E iff z in f " ].-infty,r.[ )
proof
let z be object ; :: thesis: ( z in H /\ E iff z in f " ].-infty,r.[ )
hereby :: thesis: ( z in f " ].-infty,r.[ implies z in H /\ E )
assume z in H /\ E ; :: thesis: z in f " ].-infty,r.[
then A19: ( z in H & z in E ) by XBOOLE_0:def 4;
then consider Y being set such that
A20: ( z in Y & Y in rng B ) by TARSKI:def 4;
consider x being object such that
A21: ( x in dom B & Y = B . x ) by FUNCT_1:def 3, A20;
A22: z in E /\ (B . x) by A20, A21, A19, XBOOLE_0:def 4;
A23: ex t being Point of S st
( t = x & 0 < R . x & B . x = { t1 where t1 is Point of S : ||.(t1 - t).|| < R . x } ) by A18, A21;
ex t being Point of S ex s being Real st
( t = x & s = R . x & 0 < s & ( for t1 being object st t1 in E /\ { t1 where t1 is Point of S : ||.(t1 - t).|| < s } holds
f . t1 in ].-infty,r.[ ) ) by A15, A21;
then f . z in ].-infty,r.[ by A22, A23;
hence z in f " ].-infty,r.[ by A1, A19, FUNCT_1:def 7; :: thesis: verum
end;
assume A24: z in f " ].-infty,r.[ ; :: thesis: z in H /\ E
then reconsider z0 = z as Point of S ;
A25: ( z in dom f & f . z in ].-infty,r.[ ) by A24, FUNCT_1:def 7;
consider t being Point of S such that
A26: ( t = z & 0 < R . z & B . z = { t1 where t1 is Point of S : ||.(t1 - t).|| < R . z } ) by A18, A24;
||.(z0 - z0).|| = ||.(0. S).|| by RLVECT_1:15;
then A27: z0 in B . z0 by A26;
z0 in dom B by A24, FUNCT_2:def 1;
then B . z0 in rng B by FUNCT_1:3;
then z in union (rng B) by A27, TARSKI:def 4;
hence z in H /\ E by A2, A25, XBOOLE_0:def 4; :: thesis: verum
end;
hence H /\ E = f " ].-infty,r.[ by TARSKI:2; :: thesis: H is open
for z being Point of S st z in H holds
ex N being Neighbourhood of z st N c= H
proof
let z be Point of S; :: thesis: ( z in H implies ex N being Neighbourhood of z st N c= H )
assume z in H ; :: thesis: ex N being Neighbourhood of z st N c= H
then consider Y being set such that
A28: ( z in Y & Y in rng B ) by TARSKI:def 4;
consider x being object such that
A29: ( x in dom B & Y = B . x ) by FUNCT_1:def 3, A28;
consider t being Point of S such that
A30: ( t = x & 0 < R . x & B . x = { t1 where t1 is Point of S : ||.(t1 - t).|| < R . x } ) by A18, A29;
A31: ex t1 being Point of S st
( z = t1 & ||.(t1 - t).|| < R . x ) by A30, A28, A29;
set e = (R . x) - ||.(z - t).||;
reconsider N = { y where y is Point of S : ||.(y - z).|| < (R . x) - ||.(z - t).|| } as Neighbourhood of z by A31, XREAL_1:50, NFCONT_1:3;
take N ; :: thesis: N c= H
A32: now :: thesis: for p being object st p in N holds
p in Y
let p be object ; :: thesis: ( p in N implies p in Y )
assume p in N ; :: thesis: p in Y
then consider y being Point of S such that
A33: ( y = p & ||.(y - z).|| < (R . x) - ||.(z - t).|| ) ;
A34: ||.(y - t).|| <= ||.(y - z).|| + ||.(z - t).|| by NORMSP_1:10;
||.(y - z).|| + ||.(z - t).|| < ((R . x) - ||.(z - t).||) + ||.(z - t).|| by A33, XREAL_1:8;
then ||.(y - t).|| < R . x by A34, XXREAL_0:2;
hence p in Y by A30, A29, A33; :: thesis: verum
end;
Y c= H by A28, ZFMISC_1:74;
hence N c= H by A32; :: thesis: verum
end;
hence H is open by NDIFF_1:5; :: thesis: verum