let X be non empty closed_interval Subset of REAL; for Y being RealNormSpace
for C being Subset of (R_NormSpace_of_BoundedFunctions (X,Y)) st C = ContinuousFunctions (X,Y) holds
C is closed
let Y be RealNormSpace; for C being Subset of (R_NormSpace_of_BoundedFunctions (X,Y)) st C = ContinuousFunctions (X,Y) holds
C is closed
let C be Subset of (R_NormSpace_of_BoundedFunctions (X,Y)); ( C = ContinuousFunctions (X,Y) implies C is closed )
assume A1:
C = ContinuousFunctions (X,Y)
; C is closed
now for seq being sequence of (R_NormSpace_of_BoundedFunctions (X,Y)) st rng seq c= C & seq is convergent holds
lim seq in Clet seq be
sequence of
(R_NormSpace_of_BoundedFunctions (X,Y));
( rng seq c= C & seq is convergent implies lim seq in C )assume A2:
(
rng seq c= C &
seq is
convergent )
;
lim seq in Creconsider f =
lim seq as
bounded Function of
X,
Y by RSSPACE4:def 5;
A3:
dom f = X
by FUNCT_2:def 1;
then
BoundedFunctions (
X,
Y)
c= PFuncs (
X, the
carrier of
Y)
by TARSKI:def 3;
then reconsider H =
seq as
Functional_Sequence of
X, the
carrier of
Y by FUNCT_2:7;
A4:
for
p being
Real st
p > 0 holds
ex
k being
Nat st
for
n being
Nat for
x being
set st
n >= k &
x in X holds
||.(((H . n) /. x) - (f /. x)).|| < p
dom f = X
by FUNCT_2:def 1;
then
(
dom f c= REAL &
rng f c= the
carrier of
Y )
;
then
f in PFuncs (
REAL, the
carrier of
Y)
by PARTFUN1:def 3;
then reconsider f =
f as
PartFunc of
REAL,
Y by PARTFUN1:46;
for
x0 being
Real st
x0 in dom f holds
f is_continuous_in x0
proof
let x be
Real;
( x in dom f implies f is_continuous_in x )
assume A9:
x in dom f
;
f is_continuous_in x
now for r0 being Real st 0 < r0 holds
ex w1 being Real st
( 0 < w1 & ( for z0 being Real st z0 in dom f & |.(z0 - x).| < w1 holds
||.((f /. z0) - (f /. x)).|| < r0 ) )let r0 be
Real;
( 0 < r0 implies ex w1 being Real st
( 0 < w1 & ( for z0 being Real st z0 in dom f & |.(z0 - x).| < w1 holds
||.((f /. z0) - (f /. x)).|| < r0 ) ) )assume A10:
0 < r0
;
ex w1 being Real st
( 0 < w1 & ( for z0 being Real st z0 in dom f & |.(z0 - x).| < w1 holds
||.((f /. z0) - (f /. x)).|| < r0 ) )then consider k being
Nat such that A11:
for
n being
Nat for
x being
set st
n >= k &
x in X holds
||.(((H . n) /. x) - (f /. x)).|| < r0 / 3
by A4, XREAL_1:222;
A12:
||.(((H . k) /. x) - (f /. x)).|| < r0 / 3
by A11, A3, A9;
k in NAT
by ORDINAL1:def 12;
then
k in dom seq
by NORMSP_1:12;
then
H . k in rng seq
by FUNCT_1:def 3;
then consider h being
continuous PartFunc of
REAL,
Y such that A13:
(
H . k = h &
dom h = X )
by A2, Def2, A1;
A14:
(
0 < r0 / 3 &
r0 / 3 is
Real )
by A10, XREAL_1:222;
x in dom h
by A9, A13, FUNCT_2:def 1;
then
h is_continuous_in x
by NFCONT_3:def 2;
then consider w1 being
Real such that A15:
(
0 < w1 & ( for
x0 being
Real st
x0 in dom h &
|.(x0 - x).| < w1 holds
||.((h /. x0) - (h /. x)).|| < r0 / 3 ) )
by A14, NFCONT_3:8;
take w1 =
w1;
( 0 < w1 & ( for z0 being Real st z0 in dom f & |.(z0 - x).| < w1 holds
||.((f /. z0) - (f /. x)).|| < r0 ) )thus
0 < w1
by A15;
for z0 being Real st z0 in dom f & |.(z0 - x).| < w1 holds
||.((f /. z0) - (f /. x)).|| < r0thus
for
z0 being
Real st
z0 in dom f &
|.(z0 - x).| < w1 holds
||.((f /. z0) - (f /. x)).|| < r0
verumproof
let z0 be
Real;
( z0 in dom f & |.(z0 - x).| < w1 implies ||.((f /. z0) - (f /. x)).|| < r0 )
assume A16:
(
z0 in dom f &
|.(z0 - x).| < w1 )
;
||.((f /. z0) - (f /. x)).|| < r0
then A17:
z0 in dom h
by FUNCT_2:def 1, A13;
then A18:
||.((h /. z0) - (h /. x)).|| < r0 / 3
by A16, A15;
A19:
||.((f /. x) - (h /. x)).|| < r0 / 3
by A12, A13, NORMSP_1:7;
||.((h /. z0) - (f /. z0)).|| < r0 / 3
by A17, A11, A13;
then
||.((f /. z0) - (h /. z0)).|| < r0 / 3
by NORMSP_1:7;
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) - (h /. z0)) - ((f /. x) - (h /. x))) + ((h /. z0) - (h /. x)) =
((f /. z0) - (h /. z0)) - (((f /. x) - (h /. x)) - ((h /. z0) - (h /. x)))
by RLVECT_1:29
.=
((f /. z0) - (h /. z0)) - ((f /. x) - ((h /. x) + ((h /. z0) - (h /. x))))
by RLVECT_1:27
.=
((f /. z0) - (h /. z0)) - ((f /. x) - ((h /. z0) - ((h /. x) - (h /. x))))
by RLVECT_1:29
.=
((f /. z0) - (h /. z0)) - ((f /. x) - ((h /. z0) - (0. Y)))
by RLVECT_1:15
.=
(f /. z0) - ((h /. z0) + ((f /. x) - (h /. z0)))
by RLVECT_1:27
.=
(f /. z0) - ((f /. x) - ((h /. z0) - (h /. z0)))
by RLVECT_1:29
.=
(f /. z0) - ((f /. x) - (0. Y))
by RLVECT_1:15
.=
(f /. z0) - (f /. x)
;
then A21:
||.((f /. z0) - (f /. x)).|| <= ||.(((f /. z0) - (h /. z0)) - ((f /. x) - (h /. x))).|| + ||.((h /. z0) - (h /. x)).||
by NORMSP_1:def 1;
||.(((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, NORMSP_1:3;
then
||.((f /. z0) - (f /. x)).|| <= (||.((f /. z0) - (h /. z0)).|| + ||.((f /. x) - (h /. x)).||) + ||.((h /. z0) - (h /. x)).||
by A21, XXREAL_0:2;
hence
||.((f /. z0) - (f /. x)).|| < r0
by A20, XXREAL_0:2;
verum
end; end;
hence
f is_continuous_in x
by A9, NFCONT_3:8;
verum
end; then
f is
continuous
by NFCONT_3:def 2;
hence
lim seq in C
by A3, Def2, A1;
verum end;
hence
C is closed
by NFCONT_1:def 3; verum