let a, b be real number ; :: thesis: for S1 being sequence of (Closed-Interval-MSpace a,b)
for S being sequence of RealSpace st S = S1 & a <= b holds
( ( S is convergent implies S1 is convergent ) & ( S1 is convergent implies S is convergent ) & ( S is convergent implies lim S = lim S1 ) )
let S1 be sequence of (Closed-Interval-MSpace a,b); :: thesis: for S being sequence of RealSpace st S = S1 & a <= b holds
( ( S is convergent implies S1 is convergent ) & ( S1 is convergent implies S is convergent ) & ( S is convergent implies lim S = lim S1 ) )
let S be sequence of RealSpace ; :: thesis: ( S = S1 & a <= b implies ( ( S is convergent implies S1 is convergent ) & ( S1 is convergent implies S is convergent ) & ( S is convergent implies lim S = lim S1 ) ) )
assume A1:
( S = S1 & a <= b )
; :: thesis: ( ( S is convergent implies S1 is convergent ) & ( S1 is convergent implies S is convergent ) & ( S is convergent implies lim S = lim S1 ) )
then A2:
the carrier of (Closed-Interval-MSpace a,b) = [.a,b.]
by TOPMETR:14;
reconsider P = [.a,b.] as Subset of R^1 by TOPMETR:24;
A3:
( S is convergent implies S1 is convergent )
proof
assume A4:
S is
convergent
;
:: thesis: S1 is convergent
then consider x0 being
Element of
RealSpace such that A5:
for
r being
Real st
r > 0 holds
ex
n being
Element of
NAT st
for
m being
Element of
NAT st
n <= m holds
dist (S . m),
x0 < r
by TBSP_1:def 3;
A6:
x0 = lim S
by A4, A5, TBSP_1:def 4;
A7:
for
m being
Element of
NAT holds
S . m in [.a,b.]
P is
closed
by TREAL_1:4;
then reconsider x1 =
x0 as
Element of
(Closed-Interval-MSpace a,b) by A2, A4, A6, A7, Th2, TOPMETR:def 7;
for
r being
Real st
r > 0 holds
ex
n being
Element of
NAT st
for
m being
Element of
NAT st
n <= m holds
dist (S1 . m),
x1 < r
proof
let r be
Real;
:: thesis: ( r > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist (S1 . m),x1 < r )
assume
r > 0
;
:: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist (S1 . m),x1 < r
then consider n0 being
Element of
NAT such that A8:
for
m being
Element of
NAT st
n0 <= m holds
dist (S . m),
x0 < r
by A5;
for
m being
Element of
NAT st
n0 <= m holds
dist (S1 . m),
x1 < r
proof
let m be
Element of
NAT ;
:: thesis: ( n0 <= m implies dist (S1 . m),x1 < r )
assume A9:
n0 <= m
;
:: thesis: dist (S1 . m),x1 < r
dist (S1 . m),
x1 =
the
distance of
(Closed-Interval-MSpace a,b) . (S1 . m),
x1
by METRIC_1:def 1
.=
the
distance of
RealSpace . (S1 . m),
x1
by TOPMETR:def 1
.=
dist (S . m),
x0
by A1, METRIC_1:def 1
;
hence
dist (S1 . m),
x1 < r
by A8, A9;
:: thesis: verum
end;
hence
ex
n being
Element of
NAT st
for
m being
Element of
NAT st
n <= m holds
dist (S1 . m),
x1 < r
;
:: thesis: verum
end;
hence
S1 is
convergent
by TBSP_1:def 3;
:: thesis: verum
end;
( S1 is convergent implies S is convergent )
proof
assume
S1 is
convergent
;
:: thesis: S is convergent
then consider x0 being
Element of
(Closed-Interval-MSpace a,b) such that A10:
for
r being
Real st
r > 0 holds
ex
n being
Element of
NAT st
for
m being
Element of
NAT st
n <= m holds
dist (S1 . m),
x0 < r
by TBSP_1:def 3;
x0 in [.a,b.]
by A2;
then reconsider x1 =
x0 as
Element of
RealSpace by METRIC_1:def 14;
for
r being
Real st
r > 0 holds
ex
n being
Element of
NAT st
for
m being
Element of
NAT st
n <= m holds
dist (S . m),
x1 < r
proof
let r be
Real;
:: thesis: ( r > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist (S . m),x1 < r )
assume
r > 0
;
:: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist (S . m),x1 < r
then consider n0 being
Element of
NAT such that A11:
for
m being
Element of
NAT st
n0 <= m holds
dist (S1 . m),
x0 < r
by A10;
for
m being
Element of
NAT st
n0 <= m holds
dist (S . m),
x1 < r
proof
let m be
Element of
NAT ;
:: thesis: ( n0 <= m implies dist (S . m),x1 < r )
assume A12:
n0 <= m
;
:: thesis: dist (S . m),x1 < r
dist (S1 . m),
x0 =
the
distance of
(Closed-Interval-MSpace a,b) . (S1 . m),
x0
by METRIC_1:def 1
.=
the
distance of
RealSpace . (S1 . m),
x0
by TOPMETR:def 1
.=
dist (S . m),
x1
by A1, METRIC_1:def 1
;
hence
dist (S . m),
x1 < r
by A11, A12;
:: thesis: verum
end;
hence
ex
n being
Element of
NAT st
for
m being
Element of
NAT st
n <= m holds
dist (S . m),
x1 < r
;
:: thesis: verum
end;
hence
S is
convergent
by TBSP_1:def 3;
:: thesis: verum
end;
hence
( S is convergent iff S1 is convergent )
by A3; :: thesis: ( S is convergent implies lim S = lim S1 )
thus
( S is convergent implies lim S = lim S1 )
:: thesis: verumproof
assume A13:
S is
convergent
;
:: thesis: lim S = lim S1
lim S1 in the
carrier of
(Closed-Interval-MSpace a,b)
;
then reconsider t0 =
lim S1 as
Point of
RealSpace by A2, METRIC_1:def 14;
for
r1 being
Real st
0 < r1 holds
ex
m1 being
Element of
NAT st
for
n1 being
Element of
NAT st
m1 <= n1 holds
dist (S . n1),
t0 < r1
proof
let r1 be
Real;
:: thesis: ( 0 < r1 implies ex m1 being Element of NAT st
for n1 being Element of NAT st m1 <= n1 holds
dist (S . n1),t0 < r1 )
assume
0 < r1
;
:: thesis: ex m1 being Element of NAT st
for n1 being Element of NAT st m1 <= n1 holds
dist (S . n1),t0 < r1
then consider m1 being
Element of
NAT such that A14:
for
n1 being
Element of
NAT st
m1 <= n1 holds
dist (S1 . n1),
(lim S1) < r1
by A3, A13, TBSP_1:def 4;
for
n1 being
Element of
NAT st
m1 <= n1 holds
dist (S . n1),
t0 < r1
proof
let n1 be
Element of
NAT ;
:: thesis: ( m1 <= n1 implies dist (S . n1),t0 < r1 )
assume A15:
m1 <= n1
;
:: thesis: dist (S . n1),t0 < r1
dist (S1 . n1),
(lim S1) =
the
distance of
(Closed-Interval-MSpace a,b) . (S1 . n1),
(lim S1)
by METRIC_1:def 1
.=
the
distance of
RealSpace . (S1 . n1),
(lim S1)
by TOPMETR:def 1
.=
dist (S . n1),
t0
by A1, METRIC_1:def 1
;
hence
dist (S . n1),
t0 < r1
by A14, A15;
:: thesis: verum
end;
hence
ex
m1 being
Element of
NAT st
for
n1 being
Element of
NAT st
m1 <= n1 holds
dist (S . n1),
t0 < r1
;
:: thesis: verum
end;
hence
lim S = lim S1
by A13, TBSP_1:def 4;
:: thesis: verum
end;