let x0 be Real; for f being PartFunc of REAL,REAL holds
( f is_left_convergent_in x0 iff ( ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ) & ex g being Real st
for g1 being Real st 0 < g1 holds
ex r being Real st
( r < x0 & ( for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds
|.((f . r1) - g).| < g1 ) ) ) )
let f be PartFunc of REAL,REAL; ( f is_left_convergent_in x0 iff ( ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ) & ex g being Real st
for g1 being Real st 0 < g1 holds
ex r being Real st
( r < x0 & ( for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds
|.((f . r1) - g).| < g1 ) ) ) )
thus
( f is_left_convergent_in x0 implies ( ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ) & ex g being Real st
for g1 being Real st 0 < g1 holds
ex r being Real st
( r < x0 & ( for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds
|.((f . r1) - g).| < g1 ) ) ) )
( ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ) & ex g being Real st
for g1 being Real st 0 < g1 holds
ex r being Real st
( r < x0 & ( for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds
|.((f . r1) - g).| < g1 ) ) implies f is_left_convergent_in x0 )proof
assume that A1:
f is_left_convergent_in x0
and A2:
( ex
r being
Real st
(
r < x0 & ( for
g being
Real holds
( not
r < g or not
g < x0 or not
g in dom f ) ) ) or for
g being
Real ex
g1 being
Real st
(
0 < g1 & ( for
r being
Real st
r < x0 holds
ex
r1 being
Real st
(
r < r1 &
r1 < x0 &
r1 in dom f &
|.((f . r1) - g).| >= g1 ) ) ) )
;
contradiction
consider g being
Real such that A3:
for
seq being
Real_Sequence st
seq is
convergent &
lim seq = x0 &
rng seq c= (dom f) /\ (left_open_halfline x0) holds
(
f /* seq is
convergent &
lim (f /* seq) = g )
by A1;
consider g1 being
Real such that A4:
0 < g1
and A5:
for
r being
Real st
r < x0 holds
ex
r1 being
Real st
(
r < r1 &
r1 < x0 &
r1 in dom f &
|.((f . r1) - g).| >= g1 )
by A1, A2;
defpred S1[
Nat,
Real]
means (
x0 - (1 / ($1 + 1)) < $2 & $2
< x0 & $2
in dom f &
|.((f . $2) - g).| >= g1 );
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) /\ (left_open_halfline x0)
by A12, Th5;
A14:
lim s = x0
by A12, Th5;
A15:
s is
convergent
by A12, Th5;
then A16:
lim (f /* s) = g
by A3, A14, A13;
f /* s is
convergent
by A3, 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, Th5;
then
|.((f . (s . n)) - g).| < g1
by A18, FUNCT_2:108, A19;
hence
contradiction
by A12;
verum
end;
assume A20:
for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f )
; ( for g being Real ex g1 being Real st
( 0 < g1 & ( for r being Real holds
( not r < x0 or ex r1 being Real st
( r < r1 & r1 < x0 & r1 in dom f & not |.((f . r1) - g).| < g1 ) ) ) ) or f is_left_convergent_in x0 )
given g being Real such that A21:
for g1 being Real st 0 < g1 holds
ex r being Real st
( r < x0 & ( for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds
|.((f . r1) - g).| < g1 ) )
; f is_left_convergent_in x0
now for s being Real_Sequence st s is convergent & lim s = x0 & rng s c= (dom f) /\ (left_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) /\ (left_open_halfline x0) implies ( f /* s is convergent & lim (f /* s) = g ) )assume that A22:
s is
convergent
and A23:
lim s = x0
and A24:
rng s c= (dom f) /\ (left_open_halfline x0)
;
( f /* s is convergent & lim (f /* s) = g )A25:
(dom f) /\ (left_open_halfline x0) c= dom f
by XBOOLE_1:17;
A26:
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 A27:
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 A28:
r < x0
and A29:
for
r1 being
Real st
r < r1 &
r1 < x0 &
r1 in dom f holds
|.((f . r1) - g).| < g1
by A21, A27;
consider n being
Nat such that A30:
for
k being
Nat st
n <= k holds
r < s . k
by A22, A23, A28, Th1;
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 A31:
n <= k
;
|.(((f /* s) . k) - g).| < g1A32:
s . k in rng s
by VALUED_0:28;
then
s . k in left_open_halfline x0
by A24, XBOOLE_0:def 4;
then
s . k in { g2 where g2 is Real : g2 < x0 }
by XXREAL_1:229;
then A33:
ex
g2 being
Real st
(
g2 = s . k &
g2 < x0 )
;
A34:
k in NAT
by ORDINAL1:def 12;
s . k in dom f
by A24, A32, XBOOLE_0:def 4;
then
|.((f . (s . k)) - g).| < g1
by A29, A30, A31, A33;
hence
|.(((f /* s) . k) - g).| < g1
by A24, A25, FUNCT_2:108, XBOOLE_1:1, A34;
verum end; hence
f /* s is
convergent
by SEQ_2:def 6;
lim (f /* s) = ghence
lim (f /* s) = g
by A26, SEQ_2:def 7;
verum end;
hence
f is_left_convergent_in x0
by A20; verum