let X be non empty compact TopSpace; :: thesis: for Y being Subset of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st Y = ContinuousFunctions X holds
Y is closed
let Y be Subset of (R_Normed_Algebra_of_BoundedFunctions the carrier of X); :: thesis: ( Y = ContinuousFunctions X implies Y is closed )
assume A1: Y = ContinuousFunctions X ; :: thesis: Y is closed
now :: thesis: for seq being sequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st rng seq c= Y & seq is convergent holds
lim seq in Y
let seq be sequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of X); :: thesis: ( rng seq c= Y & seq is convergent implies lim seq in Y )
assume A2: ( rng seq c= Y & seq is convergent ) ; :: thesis: lim seq in Y
lim seq in BoundedFunctions the carrier of X ;
then consider f being Function of the carrier of X,REAL such that
A3: ( f = lim seq & f | the carrier of X is bounded ) ;
now :: thesis: for z being object st z in BoundedFunctions the carrier of X holds
z in PFuncs ( the carrier of X,REAL)
let z be object ; :: thesis: ( z in BoundedFunctions the carrier of X implies z in PFuncs ( the carrier of X,REAL) )
assume z in BoundedFunctions the carrier of X ; :: thesis: z in PFuncs ( the carrier of X,REAL)
then ex f being RealMap of X st
( f = z & f | the carrier of X is bounded ) ;
hence z in PFuncs ( the carrier of X,REAL) by PARTFUN1:45; :: thesis: verum
end;
then BoundedFunctions the carrier of X c= PFuncs ( the carrier of X,REAL) ;
then reconsider H = seq as Functional_Sequence of the carrier of X,REAL by FUNCT_2:7;
A4: for p being Real st p > 0 holds
ex k being Element of NAT st
for n being Element of NAT
for x being set st n >= k & x in the carrier of X holds
|.(((H . n) . x) - (f . x)).| < p
proof
let p be Real; :: thesis: ( p > 0 implies ex k being Element of NAT st
for n being Element of NAT
for x being set st n >= k & x in the carrier of X holds
|.(((H . n) . x) - (f . x)).| < p )
assume p > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT
for x being set st n >= k & x in the carrier of X holds
|.(((H . n) . x) - (f . x)).| < p
then consider k being Nat such that
A5: for n being Nat st n >= k holds
||.((seq . n) - (lim seq)).|| < p by A2, NORMSP_1:def 7;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
take k ; :: thesis: for n being Element of NAT
for x being set st n >= k & x in the carrier of X holds
|.(((H . n) . x) - (f . x)).| < p
hereby :: thesis: verum
let n be Element of NAT ; :: thesis: for x being set st n >= k & x in the carrier of X holds
|.(((H . n) . x) - (f . x)).| < p
let x be set ; :: thesis: ( n >= k & x in the carrier of X implies |.(((H . n) . x) - (f . x)).| < p )
assume A6: ( n >= k & x in the carrier of X ) ; :: thesis: |.(((H . n) . x) - (f . x)).| < p
then A7: ||.((seq . n) - (lim seq)).|| < p by A5;
(seq . n) - (lim seq) in BoundedFunctions the carrier of X ;
then consider g being RealMap of X such that
A8: ( g = (seq . n) - (lim seq) & g | the carrier of X is bounded ) ;
seq . n in BoundedFunctions the carrier of X ;
then consider s being RealMap of X such that
A9: ( s = seq . n & s | the carrier of X is bounded ) ;
reconsider x0 = x as Element of the carrier of X by A6;
A10: g . x0 = (s . x0) - (f . x0) by A8, A9, A3, C0SP1:34;
|.(g . x0).| <= ||.((seq . n) - (lim seq)).|| by A8, C0SP1:26;
hence |.(((H . n) . x) - (f . x)).| < p by A10, A9, A7, XXREAL_0:2; :: thesis: verum
end;
end;
f is continuous
proof
for x being Point of X
for V being Subset of REAL st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V )
proof
let x be Point of X; :: thesis: for V being Subset of REAL st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V )
let V be Subset of REAL; :: thesis: ( f . x in V & V is open implies ex W being Subset of X st
( x in W & W is open & f .: W c= V ) )
set r = f . x;
assume ( f . x in V & V is open ) ; :: thesis: ex W being Subset of X st
( x in W & W is open & f .: W c= V )
then consider r0 being Real such that
A11: ( 0 < r0 & ].((f . x) - r0),((f . x) + r0).[ c= V ) by RCOMP_1:19;
consider k being Element of NAT such that
A12: for n being Element of NAT
for x being set st n >= k & x in the carrier of X holds
|.(((H . n) . x) - (f . x)).| < r0 / 3 by A4, A11, XREAL_1:222;
A13: |.(((H . k) . x) - (f . x)).| < r0 / 3 by A12;
k in NAT ;
then k in dom seq by NORMSP_1:12;
then H . k in rng seq by FUNCT_1:def 3;
then H . k in Y by A2;
then consider h being continuous RealMap of X such that
A14: H . k = h by A1;
set r1 = h . x;
set G1 = ].((h . x) - (r0 / 3)),((h . x) + (r0 / 3)).[;
A15: h . x < (h . x) + (r0 / 3) by A11, XREAL_1:29, XREAL_1:222;
then (h . x) - (r0 / 3) < h . x by XREAL_1:19;
then h . x in ].((h . x) - (r0 / 3)),((h . x) + (r0 / 3)).[ by A15;
then consider W1 being Subset of X such that
A16: ( x in W1 & W1 is open & h .: W1 c= ].((h . x) - (r0 / 3)),((h . x) + (r0 / 3)).[ ) by Th1;
now :: thesis: for x0 being object st x0 in f .: W1 holds
x0 in ].((f . x) - r0),((f . x) + r0).[
let x0 be object ; :: thesis: ( x0 in f .: W1 implies x0 in ].((f . x) - r0),((f . x) + r0).[ )
assume x0 in f .: W1 ; :: thesis: x0 in ].((f . x) - r0),((f . x) + r0).[
then consider z0 being object such that
A17: ( z0 in dom f & z0 in W1 & f . z0 = x0 ) by FUNCT_1:def 6;
h . z0 in h .: W1 by A17, FUNCT_2:35;
then ( (h . x) - (r0 / 3) < h . z0 & h . z0 < (h . x) + (r0 / 3) ) by A16, XXREAL_1:4;
then ( ((h . x) - (r0 / 3)) - (h . x) < (h . z0) - (h . x) & (h . z0) - (h . x) < ((h . x) + (r0 / 3)) - (h . x) ) by XREAL_1:9;
then A18: |.((h . z0) - (h . x)).| <= r0 / 3 by ABSVALUE:5;
A19: |.(- ((h . x) - (f . x))).| < r0 / 3 by A13, A14, COMPLEX1:52;
|.((h . z0) - (f . z0)).| < r0 / 3 by A17, A12, A14;
then |.(- ((h . z0) - (f . z0))).| < r0 / 3 by COMPLEX1:52;
then |.((f . z0) - (h . z0)).| + |.((f . x) - (h . x)).| < (r0 / 3) + (r0 / 3) by A19, XREAL_1:8;
then A20: (|.((f . z0) - (h . z0)).| + |.((f . x) - (h . x)).|) + |.((h . z0) - (h . x)).| < ((r0 / 3) + (r0 / 3)) + (r0 / 3) by A18, XREAL_1:8;
|.((f . z0) - (f . x)).| = |.((((f . z0) - (h . z0)) - ((f . x) - (h . x))) + ((h . z0) - (h . x))).| ;
then A21: |.((f . z0) - (f . x)).| <= |.(((f . z0) - (h . z0)) - ((f . x) - (h . x))).| + |.((h . z0) - (h . x)).| by COMPLEX1:56;
|.(((f . z0) - (h . z0)) - ((f . x) - (h . x))).| <= |.((f . z0) - (h . z0)).| + |.((f . x) - (h . x)).| by COMPLEX1:57;
then |.(((f . z0) - (h . z0)) - ((f . x) - (h . x))).| + |.((h . z0) - (h . x)).| <= (|.((f . z0) - (h . z0)).| + |.((f . x) - (h . x)).|) + |.((h . z0) - (h . x)).| by XREAL_1:6;
then |.((f . z0) - (f . x)).| <= (|.((f . z0) - (h . z0)).| + |.((f . x) - (h . x)).|) + |.((h . z0) - (h . x)).| by A21, XXREAL_0:2;
then |.((f . z0) - (f . x)).| < r0 by A20, XXREAL_0:2;
then ( - r0 < (f . z0) - (f . x) & (f . z0) - (f . x) < r0 ) by SEQ_2:1;
then ( (- r0) + (f . x) < ((f . z0) - (f . x)) + (f . x) & ((f . z0) - (f . x)) + (f . x) < r0 + (f . x) ) by XREAL_1:6;
hence x0 in ].((f . x) - r0),((f . x) + r0).[ by A17; :: thesis: verum
end;
then f .: W1 c= ].((f . x) - r0),((f . x) + r0).[ ;
hence ex W being Subset of X st
( x in W & W is open & f .: W c= V ) by A16, A11, XBOOLE_1:1; :: thesis: verum
end;
hence f is continuous by Th1; :: thesis: verum
end;
hence lim seq in Y by A3, A1; :: thesis: verum
end;
hence Y is closed by NFCONT_1:def 3; :: thesis: verum