let X be set ; for V, W being RealNormSpace
for H being Functional_Sequence of the carrier of V, the carrier of W st H is_unif_conv_on X & ( for n being Nat holds (H . n) | X is_continuous_on X ) holds
lim (H,X) is_continuous_on X
let V, W be RealNormSpace; for H being Functional_Sequence of the carrier of V, the carrier of W st H is_unif_conv_on X & ( for n being Nat holds (H . n) | X is_continuous_on X ) holds
lim (H,X) is_continuous_on X
let H be Functional_Sequence of the carrier of V, the carrier of W; ( H is_unif_conv_on X & ( for n being Nat holds (H . n) | X is_continuous_on X ) implies lim (H,X) is_continuous_on X )
set l = lim (H,X);
assume that
A1:
H is_unif_conv_on X
and
A2:
for n being Nat holds (H . n) | X is_continuous_on X
; lim (H,X) is_continuous_on X
A3:
H is_point_conv_on X
by A1, Th21;
then A4:
dom (lim (H,X)) = X
by Def13;
A5:
X common_on_dom H
by A1;
for x0 being Point of V st x0 in X holds
(lim (H,X)) | X is_continuous_in x0
proof
let x0 be
Point of
V;
( x0 in X implies (lim (H,X)) | X is_continuous_in x0 )
assume A6:
x0 in X
;
(lim (H,X)) | X is_continuous_in x0
then A60:
x0 in dom ((lim (H,X)) | X)
by RELAT_1:62, A4;
for
r being
Real st
0 < r holds
ex
s being
Real st
(
0 < s & ( for
x1 being
Point of
V st
x1 in dom ((lim (H,X)) | X) &
||.(x1 - x0).|| < s holds
||.((((lim (H,X)) | X) /. x1) - (((lim (H,X)) | X) /. x0)).|| < r ) )
proof
let r be
Real;
( 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of V st x1 in dom ((lim (H,X)) | X) & ||.(x1 - x0).|| < s holds
||.((((lim (H,X)) | X) /. x1) - (((lim (H,X)) | X) /. x0)).|| < r ) ) )
assume A7:
0 < r
;
ex s being Real st
( 0 < s & ( for x1 being Point of V st x1 in dom ((lim (H,X)) | X) & ||.(x1 - x0).|| < s holds
||.((((lim (H,X)) | X) /. x1) - (((lim (H,X)) | X) /. x0)).|| < r ) )
reconsider r =
r as
Element of
REAL by XREAL_0:def 1;
consider k being
Nat such that A8:
for
n being
Nat for
x1 being
Element of
V st
n >= k &
x1 in X holds
||.(((H . n) /. x1) - ((lim (H,X)) /. x1)).|| < r / 3
by A1, A7, XREAL_1:222, Th42;
0 < r / 3
by A7, XREAL_1:222;
then consider k1 being
Nat such that A9:
for
n being
Nat st
n >= k1 holds
||.(((H . n) /. x0) - ((lim (H,X)) /. x0)).|| < r / 3
by A3, A6, Th20;
reconsider m =
max (
k,
k1) as
Nat by TARSKI:1;
set h =
H . m;
A11:
dom ((H . m) | X) =
(dom (H . m)) /\ X
by RELAT_1:61
.=
X
by A5, XBOOLE_1:28
;
(H . m) | X is_continuous_on X
by A2;
then
H . m is_continuous_on X
by NFCONT_1:21;
then
(H . m) | X is_continuous_in x0
by A6, NFCONT_1:def 7;
then consider s being
Real such that A12:
0 < s
and A13:
for
x1 being
Point of
V st
x1 in dom ((H . m) | X) &
||.(x1 - x0).|| < s holds
||.((((H . m) | X) /. x1) - (((H . m) | X) /. x0)).|| < r / 3
by A7, XREAL_1:222, NFCONT_1:7;
take
s
;
( 0 < s & ( for x1 being Point of V st x1 in dom ((lim (H,X)) | X) & ||.(x1 - x0).|| < s holds
||.((((lim (H,X)) | X) /. x1) - (((lim (H,X)) | X) /. x0)).|| < r ) )
thus
0 < s
by A12;
for x1 being Point of V st x1 in dom ((lim (H,X)) | X) & ||.(x1 - x0).|| < s holds
||.((((lim (H,X)) | X) /. x1) - (((lim (H,X)) | X) /. x0)).|| < r
let x1 be
Point of
V;
( x1 in dom ((lim (H,X)) | X) & ||.(x1 - x0).|| < s implies ||.((((lim (H,X)) | X) /. x1) - (((lim (H,X)) | X) /. x0)).|| < r )
assume that A14:
x1 in dom ((lim (H,X)) | X)
and A15:
||.(x1 - x0).|| < s
;
||.((((lim (H,X)) | X) /. x1) - (((lim (H,X)) | X) /. x0)).|| < r
A16:
dom ((lim (H,X)) | X) =
(dom (lim (H,X))) /\ X
by RELAT_1:61
.=
X
by A4
;
then
||.((((H . m) | X) /. x1) - (((H . m) | X) /. x0)).|| < r / 3
by A11, A13, A14, A15;
then
||.(((H . m) /. x1) - (((H . m) | X) /. x0)).|| < r / 3
by A16, A11, A14, PARTFUN1:80;
then A17:
||.(((H . m) /. x1) - ((H . m) /. x0)).|| < r / 3
by A11, A6, PARTFUN1:80;
||.(((H . m) /. x0) - ((lim (H,X)) /. x0)).|| < r / 3
by A9, XXREAL_0:25;
then
(
||.((((H . m) /. x1) - ((H . m) /. x0)) + (((H . m) /. x0) - ((lim (H,X)) /. x0))).|| <= ||.(((H . m) /. x1) - ((H . m) /. x0)).|| + ||.(((H . m) /. x0) - ((lim (H,X)) /. x0)).|| &
||.(((H . m) /. x1) - ((H . m) /. x0)).|| + ||.(((H . m) /. x0) - ((lim (H,X)) /. x0)).|| < (r / 3) + (r / 3) )
by A17, NORMSP_1:def 1, XREAL_1:8;
then A18:
||.((((H . m) /. x1) - ((H . m) /. x0)) + (((H . m) /. x0) - ((lim (H,X)) /. x0))).|| < (r / 3) + (r / 3)
by XXREAL_0:2;
||.(((lim (H,X)) /. x1) - ((lim (H,X)) /. x0)).|| =
||.(((((lim (H,X)) /. x1) - ((H . m) /. x1)) + ((H . m) /. x1)) - ((lim (H,X)) /. x0)).||
by RLVECT_4:1
.=
||.((((lim (H,X)) /. x1) - ((H . m) /. x1)) + (((H . m) /. x1) - ((lim (H,X)) /. x0))).||
by RLVECT_1:28
.=
||.((((lim (H,X)) /. x1) - ((H . m) /. x1)) + (((((H . m) /. x1) - ((H . m) /. x0)) + ((H . m) /. x0)) - ((lim (H,X)) /. x0))).||
by RLVECT_4:1
.=
||.((((lim (H,X)) /. x1) - ((H . m) /. x1)) + ((((H . m) /. x1) - ((H . m) /. x0)) + (((H . m) /. x0) - ((lim (H,X)) /. x0)))).||
by RLVECT_1:28
;
then A19:
||.(((lim (H,X)) /. x1) - ((lim (H,X)) /. x0)).|| <= ||.(((lim (H,X)) /. x1) - ((H . m) /. x1)).|| + ||.((((H . m) /. x1) - ((H . m) /. x0)) + (((H . m) /. x0) - ((lim (H,X)) /. x0))).||
by NORMSP_1:def 1;
||.(((H . m) /. x1) - ((lim (H,X)) /. x1)).|| < r / 3
by A8, A16, A14, XXREAL_0:25;
then
||.(- (((lim (H,X)) /. x1) - ((H . m) /. x1))).|| < r / 3
by RLVECT_1:33;
then
||.(((lim (H,X)) /. x1) - ((H . m) /. x1)).|| < r / 3
by NORMSP_1:2;
then
||.(((lim (H,X)) /. x1) - ((H . m) /. x1)).|| + ||.((((H . m) /. x1) - ((H . m) /. x0)) + (((H . m) /. x0) - ((lim (H,X)) /. x0))).|| < (r / 3) + ((r / 3) + (r / 3))
by A18, XREAL_1:8;
then
||.(((lim (H,X)) /. x1) - ((lim (H,X)) /. x0)).|| < ((r / 3) + (r / 3)) + (r / 3)
by A19, XXREAL_0:2;
then
||.((((lim (H,X)) | X) /. x1) - ((lim (H,X)) /. x0)).|| < r
by A14, PARTFUN1:80;
hence
||.((((lim (H,X)) | X) /. x1) - (((lim (H,X)) | X) /. x0)).|| < r
by A4, RELAT_1:68;
verum
end;
hence
(lim (H,X)) | X is_continuous_in x0
by NFCONT_1:7, A60;
verum
end;
hence
lim (H,X) is_continuous_on X
by NFCONT_1:def 7, A4; verum