let T be non empty TopSpace; for FS1 being Functional_Sequence of the carrier of T,REAL st ( for n being Nat ex f being RealMap of T st
( FS1 . n = f & f is continuous & ( for p being Point of T holds f . p >= 0 ) ) ) & ex seq being Real_Sequence st
( seq is summable & ( for n being Nat
for p being Point of T holds (FS1 # p) . n <= seq . n ) ) holds
for f being RealMap of T st ( for p being Point of T holds f . p = Sum (FS1 # p) ) holds
f is continuous
let FS1 be Functional_Sequence of the carrier of T,REAL; ( ( for n being Nat ex f being RealMap of T st
( FS1 . n = f & f is continuous & ( for p being Point of T holds f . p >= 0 ) ) ) & ex seq being Real_Sequence st
( seq is summable & ( for n being Nat
for p being Point of T holds (FS1 # p) . n <= seq . n ) ) implies for f being RealMap of T st ( for p being Point of T holds f . p = Sum (FS1 # p) ) holds
f is continuous )
assume that
A1:
for n being Nat ex f being RealMap of T st
( FS1 . n = f & f is continuous & ( for p being Point of T holds f . p >= 0 ) )
and
A2:
ex seq being Real_Sequence st
( seq is summable & ( for n being Nat
for p being Point of T holds (FS1 # p) . n <= seq . n ) )
; for f being RealMap of T st ( for p being Point of T holds f . p = Sum (FS1 # p) ) holds
f is continuous
let f be RealMap of T; ( ( for p being Point of T holds f . p = Sum (FS1 # p) ) implies f is continuous )
assume A3:
for p being Point of T holds f . p = Sum (FS1 # p)
; f is continuous
reconsider fR = f as Function of T,R^1 by TOPMETR:17;
now for p being Point of T holds fR is_continuous_at plet p be
Point of
T;
fR is_continuous_at p
for
R being
Subset of
R^1 st
R is
open &
fR . p in R holds
ex
U being
Subset of
T st
(
U is
open &
p in U &
fR .: U c= R )
proof
reconsider fRp =
fR . p as
Point of
RealSpace by METRIC_1:def 13, XREAL_0:def 1;
let R be
Subset of
R^1;
( R is open & fR . p in R implies ex U being Subset of T st
( U is open & p in U & fR .: U c= R ) )
assume
(
R is
open &
fR . p in R )
;
ex U being Subset of T st
( U is open & p in U & fR .: U c= R )
then consider rn being
Real such that A4:
rn > 0
and A5:
Ball (
fRp,
rn)
c= R
by TOPMETR:15, TOPMETR:def 6;
set r2 =
rn / 2;
set r4 =
rn / 4;
reconsider r2 =
rn / 2,
r4 =
rn / 4 as
Real ;
A6:
r4 > 0
by A4, XREAL_1:224;
consider seq being
Real_Sequence such that A7:
seq is
summable
and A8:
for
n being
Nat for
q being
Point of
T holds
(FS1 # q) . n <= seq . n
by A2;
Partial_Sums seq is
convergent
by A7, SERIES_1:def 2;
then consider n being
Nat such that A9:
for
m being
Nat st
n <= m holds
|.(((Partial_Sums seq) . m) - (lim (Partial_Sums seq))).| < r4
by A6, SEQ_2:def 7;
defpred S1[
object ,
object ]
means ex
SS being
Subset of
T st
(
SS = $2 &
SS is
open &
p in SS & ( for
f1 being
RealMap of
T st
FS1 . $1
= f1 holds
for
f1p being
Point of
RealSpace st
f1p = f1 . p holds
f1 .: SS c= Ball (
f1p,
(r2 / (n + 1))) ) );
A10:
for
k being
object st
k in {0} \/ (Seg n) holds
ex
U being
object st
(
U in bool the
carrier of
T &
S1[
k,
U] )
proof
let k be
object ;
( k in {0} \/ (Seg n) implies ex U being object st
( U in bool the carrier of T & S1[k,U] ) )
assume
k in {0} \/ (Seg n)
;
ex U being object st
( U in bool the carrier of T & S1[k,U] )
then
(
k in Seg n or
k in {0} )
by XBOOLE_0:def 3;
then reconsider k =
k as
Element of
NAT by TARSKI:def 1;
consider f1 being
RealMap of
T such that A11:
FS1 . k = f1
and A12:
f1 is
continuous
and
for
p being
Point of
T holds
f1 . p >= 0
by A1;
reconsider f19 =
f1 as
Function of
T,
R^1 by TOPMETR:17;
reconsider f1p =
f19 . p as
Point of
RealSpace by METRIC_1:def 13, XREAL_0:def 1;
set B =
Ball (
f1p,
(r2 / (n + 1)));
reconsider B =
Ball (
f1p,
(r2 / (n + 1))) as
Subset of
R^1 by METRIC_1:def 13, TOPMETR:17;
(
dist (
f1p,
f1p)
= 0 &
r2 > 0 )
by A4, METRIC_1:1, XREAL_1:215;
then
dist (
f1p,
f1p)
< r2 / (n + 1)
by XREAL_1:139;
then A13:
f1p in B
by METRIC_1:11;
f19 is
continuous
by A12, JORDAN5A:27;
then
(
B is
open &
f19 is_continuous_at p )
by TMAP_1:50, TOPMETR:14, TOPMETR:def 6;
then consider U being
Subset of
T such that A14:
(
U is
open &
p in U )
and A15:
f19 .: U c= B
by A13, TMAP_1:43;
for
f1 being
RealMap of
T st
FS1 . k = f1 holds
for
f1p being
Point of
RealSpace st
f1p = f1 . p holds
f1 .: U c= Ball (
f1p,
(r2 / (n + 1)))
by A11, A15;
hence
ex
U being
object st
(
U in bool the
carrier of
T &
S1[
k,
U] )
by A14;
verum
end;
consider FSn being
Function of
({0} \/ (Seg n)),
(bool the carrier of T) such that A16:
for
k being
object st
k in {0} \/ (Seg n) holds
S1[
k,
FSn . k]
from FUNCT_2:sch 1(A10);
A17:
for
k being
Nat for
q being
Point of
T holds
(FS1 # q) . k >= 0
A18:
for
k being
Nat holds
(seq ^\ (n + 1)) . k >= 0
reconsider RNG =
rng FSn as
Subset-Family of
T ;
A19:
RNG is
open
0 in {0}
by TARSKI:def 1;
then
0 in {0} \/ (Seg n)
by XBOOLE_0:def 3;
then reconsider RNG =
RNG as non
empty Subset-Family of
T by FUNCT_2:4;
A22:
(
lim (Partial_Sums seq) = Sum seq &
Sum seq = ((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1))) )
by A7, SERIES_1:15, SERIES_1:def 3;
|.(((Partial_Sums seq) . n) - (lim (Partial_Sums seq))).| < r4
by A9;
then
|.(- (Sum (seq ^\ (n + 1)))).| < r4
by A22;
then A23:
|.(Sum (seq ^\ (n + 1))).| < r4
by COMPLEX1:52;
seq ^\ (n + 1) is
summable
by A7, SERIES_1:12;
then
Sum (seq ^\ (n + 1)) >= 0
by A18, SERIES_1:18;
then A24:
Sum (seq ^\ (n + 1)) < r4
by A23, ABSVALUE:def 1;
A25:
for
q being
Point of
T holds
(
FS1 # q is
summable &
0 <= Sum ((FS1 # q) ^\ (n + 1)) &
Sum ((FS1 # q) ^\ (n + 1)) < r4 )
proof
let q be
Point of
T;
( FS1 # q is summable & 0 <= Sum ((FS1 # q) ^\ (n + 1)) & Sum ((FS1 # q) ^\ (n + 1)) < r4 )
set F =
FS1 # q;
A28:
for
k being
Nat holds
(
0 <= (FS1 # q) . k &
(FS1 # q) . k <= seq . k )
by A8, A17;
then
FS1 # q is
summable
by A7, SERIES_1:20;
then A29:
(FS1 # q) ^\ (n + 1) is
summable
by SERIES_1:12;
seq ^\ (n + 1) is
summable
by A7, SERIES_1:12;
then
Sum ((FS1 # q) ^\ (n + 1)) <= Sum (seq ^\ (n + 1))
by A26, SERIES_1:20;
hence
(
FS1 # q is
summable &
0 <= Sum ((FS1 # q) ^\ (n + 1)) &
Sum ((FS1 # q) ^\ (n + 1)) < r4 )
by A7, A24, A28, A26, A29, SERIES_1:18, SERIES_1:20, XXREAL_0:2;
verum
end;
A30:
fR .: (meet RNG) c= R
proof
let fRq be
object ;
TARSKI:def 3 ( not fRq in fR .: (meet RNG) or fRq in R )
assume
fRq in fR .: (meet RNG)
;
fRq in R
then consider q being
object such that A31:
q in dom fR
and A32:
q in meet RNG
and A33:
fRq = fR . q
by FUNCT_1:def 6;
reconsider q =
q as
Point of
T by A31;
set sp =
FS1 # p;
set sq =
FS1 # q;
set spn =
(FS1 # p) ^\ (n + 1);
set sqn =
(FS1 # q) ^\ (n + 1);
set absPSpq =
Partial_Sums |.((FS1 # p) - (FS1 # q)).|;
for
k being
Nat st
k <= n holds
|.((FS1 # p) - (FS1 # q)).| . k <= r2 / (n + 1)
proof
let k be
Nat;
( k <= n implies |.((FS1 # p) - (FS1 # q)).| . k <= r2 / (n + 1) )
assume A34:
k <= n
;
|.((FS1 # p) - (FS1 # q)).| . k <= r2 / (n + 1)
(
k = 0 or
k >= 1 )
by NAT_1:14;
then
(
k in {0} or
k in Seg n )
by A34, FINSEQ_1:1, TARSKI:def 1;
then A35:
k in {0} \/ (Seg n)
by XBOOLE_0:def 3;
then
FSn . k in RNG
by FUNCT_2:4;
then A36:
q in FSn . k
by A32, SETFAM_1:def 1;
A37:
k in NAT
by ORDINAL1:def 12;
dom ((FS1 # p) - (FS1 # q)) = NAT
by FUNCT_2:def 1;
then A38:
((FS1 # p) - (FS1 # q)) . k = ((FS1 # p) . k) - ((FS1 # q) . k)
by VALUED_1:13, A37;
consider f1 being
RealMap of
T such that A39:
FS1 . k = f1
and
f1 is
continuous
and
for
p being
Point of
T holds
f1 . p >= 0
by A1;
reconsider f1p =
f1 . p,
f1q =
f1 . q as
Point of
RealSpace by METRIC_1:def 13;
ex
SS being
Subset of
T st
(
SS = FSn . k &
SS is
open &
p in SS & ( for
f1 being
RealMap of
T st
FS1 . k = f1 holds
for
f1p being
Point of
RealSpace st
f1p = f1 . p holds
f1 .: SS c= Ball (
f1p,
(r2 / (n + 1))) ) )
by A16, A35;
then A40:
f1 .: (FSn . k) c= Ball (
f1p,
(r2 / (n + 1)))
by A39;
dom f1 = the
carrier of
T
by FUNCT_2:def 1;
then
f1q in f1 .: (FSn . k)
by A36, FUNCT_1:def 6;
then
dist (
f1p,
f1q)
< r2 / (n + 1)
by A40, METRIC_1:11;
then A41:
|.((f1 . p) - (f1 . q)).| < r2 / (n + 1)
by TOPMETR:11;
f1 . p = (FS1 # p) . k
by A39, SEQFUNC:def 10;
then
|.(((FS1 # p) . k) - ((FS1 # q) . k)).| < r2 / (n + 1)
by A39, A41, SEQFUNC:def 10;
hence
|.((FS1 # p) - (FS1 # q)).| . k <= r2 / (n + 1)
by A38, SEQ_1:12;
verum
end;
then A42:
(Partial_Sums |.((FS1 # p) - (FS1 # q)).|) . n <= (r2 / (n + 1)) * (n + 1)
by Th12;
A43:
n in NAT
by ORDINAL1:def 12;
set PSp =
Partial_Sums (FS1 # p);
set PSq =
Partial_Sums (FS1 # q);
set PSpq =
Partial_Sums ((FS1 # p) - (FS1 # q));
(
(Partial_Sums (FS1 # p)) - (Partial_Sums (FS1 # q)) = Partial_Sums ((FS1 # p) - (FS1 # q)) &
dom ((Partial_Sums (FS1 # p)) - (Partial_Sums (FS1 # q))) = NAT )
by SEQ_1:1, SERIES_1:6;
then A44:
|.(((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)).| = |.((Partial_Sums ((FS1 # p) - (FS1 # q))) . n).|
by VALUED_1:13, A43;
|.((Partial_Sums ((FS1 # p) - (FS1 # q))) . n).| <= (Partial_Sums |.((FS1 # p) - (FS1 # q)).|) . n
by Th13;
then
|.(((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)).| <= (r2 / (n + 1)) * (n + 1)
by A44, A42, XXREAL_0:2;
then A45:
|.(((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)).| <= r2
by XCMPLX_1:87;
0 <= Sum ((FS1 # p) ^\ (n + 1))
by A25;
then A46:
|.(Sum ((FS1 # p) ^\ (n + 1))).| = Sum ((FS1 # p) ^\ (n + 1))
by ABSVALUE:def 1;
0 <= Sum ((FS1 # q) ^\ (n + 1))
by A25;
then A47:
|.(Sum ((FS1 # q) ^\ (n + 1))).| = Sum ((FS1 # q) ^\ (n + 1))
by ABSVALUE:def 1;
reconsider fRq =
fR . q as
Point of
RealSpace by METRIC_1:def 13, XREAL_0:def 1;
A48:
|.((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1)))).| <= |.(Sum ((FS1 # p) ^\ (n + 1))).| + |.(Sum ((FS1 # q) ^\ (n + 1))).|
by COMPLEX1:57;
A49:
(
fRp = Sum (FS1 # p) &
fRq = Sum (FS1 # q) )
by A3;
(
Sum (FS1 # p) = ((Partial_Sums (FS1 # p)) . n) + (Sum ((FS1 # p) ^\ (n + 1))) &
Sum (FS1 # q) = ((Partial_Sums (FS1 # q)) . n) + (Sum ((FS1 # q) ^\ (n + 1))) )
by A25, SERIES_1:15;
then
|.((fR . p) - (fR . q)).| = |.((((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)) + ((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1))))).|
by A49;
then A50:
|.((fR . p) - (fR . q)).| <= |.(((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)).| + |.((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1)))).|
by COMPLEX1:56;
(
Sum ((FS1 # p) ^\ (n + 1)) < r4 &
Sum ((FS1 # q) ^\ (n + 1)) < r4 )
by A25;
then
|.(Sum ((FS1 # p) ^\ (n + 1))).| + |.(Sum ((FS1 # q) ^\ (n + 1))).| < r4 + r4
by A46, A47, XREAL_1:8;
then
|.((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1)))).| < r2
by A48, XXREAL_0:2;
then
|.(((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)).| + |.((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1)))).| < r2 + r2
by A45, XREAL_1:8;
then
|.((fR . p) - (fR . q)).| < rn
by A50, XXREAL_0:2;
then
dist (
fRp,
fRq)
< rn
by TOPMETR:11;
then
fRq in Ball (
fRp,
rn)
by METRIC_1:11;
hence
fRq in R
by A5, A33;
verum
end;
now for Fx being set st Fx in RNG holds
p in Fxend;
then
p in meet RNG
by SETFAM_1:def 1;
hence
ex
U being
Subset of
T st
(
U is
open &
p in U &
fR .: U c= R )
by A19, A30, TOPS_2:20;
verum
end; hence
fR is_continuous_at p
by TMAP_1:43;
verum end;
then
fR is continuous
by TMAP_1:50;
hence
f is continuous
by JORDAN5A:27; verum