let g, x0 be Real; for f being PartFunc of REAL,REAL st f is_right_convergent_in x0 holds
( lim_right (f,x0) = g iff for g1 being Real st 0 < g1 holds
ex r being Real st
( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
|.((f . r1) - g).| < g1 ) ) )
let f be PartFunc of REAL,REAL; ( f is_right_convergent_in x0 implies ( lim_right (f,x0) = g iff for g1 being Real st 0 < g1 holds
ex r being Real st
( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
|.((f . r1) - g).| < g1 ) ) ) )
assume A1:
f is_right_convergent_in x0
; ( lim_right (f,x0) = g iff for g1 being Real st 0 < g1 holds
ex r being Real st
( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
|.((f . r1) - g).| < g1 ) ) )
thus
( lim_right (f,x0) = g implies for g1 being Real st 0 < g1 holds
ex r being Real st
( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
|.((f . r1) - g).| < g1 ) ) )
( ( for g1 being Real st 0 < g1 holds
ex r being Real st
( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
|.((f . r1) - g).| < g1 ) ) ) implies lim_right (f,x0) = g )proof
assume that A2:
lim_right (
f,
x0)
= g
and A3:
ex
g1 being
Real st
(
0 < g1 & ( for
r being
Real st
x0 < r holds
ex
r1 being
Real st
(
r1 < r &
x0 < r1 &
r1 in dom f &
|.((f . r1) - g).| >= g1 ) ) )
;
contradiction
consider g1 being
Real such that A4:
0 < g1
and A5:
for
r being
Real st
x0 < r holds
ex
r1 being
Real st
(
r1 < r &
x0 < r1 &
r1 in dom f &
|.((f . r1) - g).| >= g1 )
by A3;
defpred S1[
Nat,
Real]
means (
x0 < $2 & $2
< x0 + (1 / ($1 + 1)) & $2
in dom f &
g1 <= |.((f . $2) - g).| );
consider s being
Real_Sequence such that A11:
for
n being
Element of
NAT holds
S1[
n,
s . n]
from FUNCT_2:sch 3(A6);
A12:
for
n being
Nat holds
S1[
n,
s . n]
A13:
rng s c= (dom f) /\ (right_open_halfline x0)
by A12, Th6;
A14:
lim s = x0
by A12, Th6;
A15:
s is
convergent
by A12, Th6;
then A16:
lim (f /* s) = g
by A1, A2, A14, A13, Def8;
f /* s is
convergent
by A1, A15, A14, A13;
then consider n being
Nat such that A17:
for
k being
Nat st
n <= k holds
|.(((f /* s) . k) - g).| < g1
by A4, A16, SEQ_2:def 7;
A18:
|.(((f /* s) . n) - g).| < g1
by A17;
A19:
n in NAT
by ORDINAL1:def 12;
rng s c= dom f
by A12, Th6;
then
|.((f . (s . n)) - g).| < g1
by A18, FUNCT_2:108, A19;
hence
contradiction
by A12;
verum
end;
assume A20:
for g1 being Real st 0 < g1 holds
ex r being Real st
( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
|.((f . r1) - g).| < g1 ) )
; lim_right (f,x0) = g
reconsider g = g as Real ;
now for s being Real_Sequence st s is convergent & lim s = x0 & rng s c= (dom f) /\ (right_open_halfline x0) holds
( f /* s is convergent & lim (f /* s) = g )let s be
Real_Sequence;
( s is convergent & lim s = x0 & rng s c= (dom f) /\ (right_open_halfline x0) implies ( f /* s is convergent & lim (f /* s) = g ) )assume that A21:
s is
convergent
and A22:
lim s = x0
and A23:
rng s c= (dom f) /\ (right_open_halfline x0)
;
( f /* s is convergent & lim (f /* s) = g )A24:
(dom f) /\ (right_open_halfline x0) c= dom f
by XBOOLE_1:17;
A25:
now for g1 being Real st 0 < g1 holds
ex n being Nat st
for k being Nat st n <= k holds
|.(((f /* s) . k) - g).| < g1let g1 be
Real;
( 0 < g1 implies ex n being Nat st
for k being Nat st n <= k holds
|.(((f /* s) . k) - g).| < g1 )assume A26:
0 < g1
;
ex n being Nat st
for k being Nat st n <= k holds
|.(((f /* s) . k) - g).| < g1consider r being
Real such that A27:
x0 < r
and A28:
for
r1 being
Real st
r1 < r &
x0 < r1 &
r1 in dom f holds
|.((f . r1) - g).| < g1
by A20, A26;
consider n being
Nat such that A29:
for
k being
Nat st
n <= k holds
s . k < r
by A21, A22, A27, Th2;
take n =
n;
for k being Nat st n <= k holds
|.(((f /* s) . k) - g).| < g1let k be
Nat;
( n <= k implies |.(((f /* s) . k) - g).| < g1 )assume A30:
n <= k
;
|.(((f /* s) . k) - g).| < g1A31:
s . k in rng s
by VALUED_0:28;
then
s . k in right_open_halfline x0
by A23, XBOOLE_0:def 4;
then
s . k in { g2 where g2 is Real : x0 < g2 }
by XXREAL_1:230;
then A32:
ex
g2 being
Real st
(
g2 = s . k &
x0 < g2 )
;
A33:
k in NAT
by ORDINAL1:def 12;
s . k in dom f
by A23, A31, XBOOLE_0:def 4;
then
|.((f . (s . k)) - g).| < g1
by A28, A29, A30, A32;
hence
|.(((f /* s) . k) - g).| < g1
by A23, A24, FUNCT_2:108, XBOOLE_1:1, A33;
verum end; hence
f /* s is
convergent
by SEQ_2:def 6;
lim (f /* s) = ghence
lim (f /* s) = g
by A25, SEQ_2:def 7;
verum end;
hence
lim_right (f,x0) = g
by A1, Def8; verum