let X be set ; :: thesis: for H being Functional_Sequence of REAL ,REAL st H is_unif_conv_on X & ( for n being Element of NAT holds (H . n) | X is continuous ) holds
(lim H,X) | X is continuous
let H be Functional_Sequence of REAL ,REAL ; :: thesis: ( H is_unif_conv_on X & ( for n being Element of NAT holds (H . n) | X is continuous ) implies (lim H,X) | X is continuous )
set l = lim H,X;
assume A1:
( H is_unif_conv_on X & ( for n being Element of NAT holds (H . n) | X is continuous ) )
; :: thesis: (lim H,X) | X is continuous
then A2:
H is_point_conv_on X
by Th23;
then A3:
dom (lim H,X) = X
by Def14;
A4:
X common_on_dom H
by A1, Def13;
for x0 being real number st x0 in dom ((lim H,X) | X) holds
(lim H,X) | X is_continuous_in x0
proof
let x0 be
real number ;
:: thesis: ( x0 in dom ((lim H,X) | X) implies (lim H,X) | X is_continuous_in x0 )
assume
x0 in dom ((lim H,X) | X)
;
:: thesis: (lim H,X) | X is_continuous_in x0
then B5:
x0 in X
by RELAT_1:86;
reconsider x0 =
x0 as
Real by XREAL_0:def 1;
for
r being
real number st
0 < r holds
ex
s being
real number st
(
0 < s & ( for
x1 being
real number st
x1 in dom ((lim H,X) | X) &
abs (x1 - x0) < s holds
abs ((((lim H,X) | X) . x1) - (((lim H,X) | X) . x0)) < r ) )
proof
let r be
real number ;
:: thesis: ( 0 < r implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom ((lim H,X) | X) & abs (x1 - x0) < s holds
abs ((((lim H,X) | X) . x1) - (((lim H,X) | X) . x0)) < r ) ) )
assume
0 < r
;
:: thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom ((lim H,X) | X) & abs (x1 - x0) < s holds
abs ((((lim H,X) | X) . x1) - (((lim H,X) | X) . x0)) < r ) )
then A7:
0 < r / 3
by XREAL_1:224;
reconsider r =
r as
Real by XREAL_0:def 1;
consider k being
Element of
NAT such that A8:
for
n being
Element of
NAT for
x1 being
Real st
n >= k &
x1 in X holds
abs (((H . n) . x1) - ((lim H,X) . x1)) < r / 3
by A1, A7, Th44;
consider k1 being
Element of
NAT such that A9:
for
n being
Element of
NAT st
n >= k1 holds
abs (((H . n) . x0) - ((lim H,X) . x0)) < r / 3
by A2, A7, Th22, B5;
set m =
max k,
k1;
set h =
H . (max k,k1);
A11:
dom ((lim H,X) | X) =
(dom (lim H,X)) /\ X
by RELAT_1:90
.=
X
by A3
;
A14:
(
X c= dom (H . (max k,k1)) &
X c= X )
by A4, Def10;
A15:
dom ((H . (max k,k1)) | X) =
(dom (H . (max k,k1))) /\ X
by RELAT_1:90
.=
X
by A14, XBOOLE_1:28
;
(H . (max k,k1)) | X is
continuous
by A1;
then
(H . (max k,k1)) | X is_continuous_in x0
by B5, A15, FCONT_1:def 2;
then consider s being
real number such that A10:
(
0 < s & ( for
x1 being
real number st
x1 in dom ((H . (max k,k1)) | X) &
abs (x1 - x0) < s holds
abs ((((H . (max k,k1)) | X) . x1) - (((H . (max k,k1)) | X) . x0)) < r / 3 ) )
by A7, FCONT_1:3;
reconsider s =
s as
Real by XREAL_0:def 1;
take
s
;
:: thesis: ( 0 < s & ( for x1 being real number st x1 in dom ((lim H,X) | X) & abs (x1 - x0) < s holds
abs ((((lim H,X) | X) . x1) - (((lim H,X) | X) . x0)) < r ) )
thus
0 < s
by A10;
:: thesis: for x1 being real number st x1 in dom ((lim H,X) | X) & abs (x1 - x0) < s holds
abs ((((lim H,X) | X) . x1) - (((lim H,X) | X) . x0)) < r
let x1 be
real number ;
:: thesis: ( x1 in dom ((lim H,X) | X) & abs (x1 - x0) < s implies abs ((((lim H,X) | X) . x1) - (((lim H,X) | X) . x0)) < r )
assume A12:
(
x1 in dom ((lim H,X) | X) &
abs (x1 - x0) < s )
;
:: thesis: abs ((((lim H,X) | X) . x1) - (((lim H,X) | X) . x0)) < r
then
abs (((H . (max k,k1)) . x1) - ((lim H,X) . x1)) < r / 3
by A8, A11, XXREAL_0:25;
then
abs (- (((lim H,X) . x1) - ((H . (max k,k1)) . x1))) < r / 3
;
then A13:
abs (((lim H,X) . x1) - ((H . (max k,k1)) . x1)) < r / 3
by COMPLEX1:138;
abs ((((H . (max k,k1)) | X) . x1) - (((H . (max k,k1)) | X) . x0)) < r / 3
by A10, A11, A12, A15;
then
abs (((H . (max k,k1)) . x1) - (((H . (max k,k1)) | X) . x0)) < r / 3
by A11, A12, A15, FUNCT_1:70;
then A16:
abs (((H . (max k,k1)) . x1) - ((H . (max k,k1)) . x0)) < r / 3
by B5, FUNCT_1:72;
A17:
abs (((H . (max k,k1)) . x0) - ((lim H,X) . x0)) < r / 3
by A9, XXREAL_0:25;
abs (((lim H,X) . x1) - ((lim H,X) . x0)) = abs ((((lim H,X) . x1) - ((H . (max k,k1)) . x1)) + ((((H . (max k,k1)) . x1) - ((H . (max k,k1)) . x0)) + (((H . (max k,k1)) . x0) - ((lim H,X) . x0))))
;
then A18:
abs (((lim H,X) . x1) - ((lim H,X) . x0)) <= (abs (((lim H,X) . x1) - ((H . (max k,k1)) . x1))) + (abs ((((H . (max k,k1)) . x1) - ((H . (max k,k1)) . x0)) + (((H . (max k,k1)) . x0) - ((lim H,X) . x0))))
by COMPLEX1:142;
A19:
abs ((((H . (max k,k1)) . x1) - ((H . (max k,k1)) . x0)) + (((H . (max k,k1)) . x0) - ((lim H,X) . x0))) <= (abs (((H . (max k,k1)) . x1) - ((H . (max k,k1)) . x0))) + (abs (((H . (max k,k1)) . x0) - ((lim H,X) . x0)))
by COMPLEX1:142;
(abs (((H . (max k,k1)) . x1) - ((H . (max k,k1)) . x0))) + (abs (((H . (max k,k1)) . x0) - ((lim H,X) . x0))) < (r / 3) + (r / 3)
by A16, A17, XREAL_1:10;
then
abs ((((H . (max k,k1)) . x1) - ((H . (max k,k1)) . x0)) + (((H . (max k,k1)) . x0) - ((lim H,X) . x0))) < (r / 3) + (r / 3)
by A19, XXREAL_0:2;
then
(abs (((lim H,X) . x1) - ((H . (max k,k1)) . x1))) + (abs ((((H . (max k,k1)) . x1) - ((H . (max k,k1)) . x0)) + (((H . (max k,k1)) . x0) - ((lim H,X) . x0)))) < (r / 3) + ((r / 3) + (r / 3))
by A13, XREAL_1:10;
then
abs (((lim H,X) . x1) - ((lim H,X) . x0)) < ((r / 3) + (r / 3)) + (r / 3)
by A18, XXREAL_0:2;
then
abs ((((lim H,X) | X) . x1) - ((lim H,X) . x0)) < r
by A12, FUNCT_1:70;
hence
abs ((((lim H,X) | X) . x1) - (((lim H,X) | X) . x0)) < r
by A3, RELAT_1:97;
:: thesis: verum
end;
hence
(lim H,X) | X is_continuous_in x0
by FCONT_1:3;
:: thesis: verum
end;
hence
(lim H,X) | X is continuous
by FCONT_1:def 2; :: thesis: verum