let x0 be Real; for f being PartFunc of REAL,REAL holds
( f is_convergent_in x0 iff ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ex g being Real st
for g1 being Real st 0 < g1 holds
ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f holds
|.((f . r1) - g).| < g1 ) ) ) )
let f be PartFunc of REAL,REAL; ( f is_convergent_in x0 iff ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ex g being Real st
for g1 being Real st 0 < g1 holds
ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f holds
|.((f . r1) - g).| < g1 ) ) ) )
thus
( f is_convergent_in x0 implies ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ex g being Real st
for g1 being Real st 0 < g1 holds
ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f holds
|.((f . r1) - g).| < g1 ) ) ) )
( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ex g being Real st
for g1 being Real st 0 < g1 holds
ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f holds
|.((f . r1) - g).| < g1 ) ) implies f is_convergent_in x0 )proof
assume that A1:
f is_convergent_in x0
and A2:
( ex
r1,
r2 being
Real st
(
r1 < x0 &
x0 < r2 & ( for
g1,
g2 being
Real holds
( not
r1 < g1 or not
g1 < x0 or not
g1 in dom f or not
g2 < r2 or not
x0 < g2 or not
g2 in dom f ) ) ) or for
g being
Real ex
g1 being
Real st
(
0 < g1 & ( for
g2 being
Real st
0 < g2 holds
ex
r1 being
Real st
(
0 < |.(x0 - r1).| &
|.(x0 - r1).| < g2 &
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) \ {x0} holds
(
f /* seq is
convergent &
lim (f /* seq) = g )
by A1;
consider g1 being
Real such that A4:
0 < g1
and A5:
for
g2 being
Real st
0 < g2 holds
ex
r1 being
Real st
(
0 < |.(x0 - r1).| &
|.(x0 - r1).| < g2 &
r1 in dom f &
|.((f . r1) - g).| >= g1 )
by A1, A2;
defpred S1[
Element of
NAT ,
Real]
means (
0 < |.(x0 - $2).| &
|.(x0 - $2).| < 1
/ ($1 + 1) & $2
in dom f &
|.((f . $2) - g).| >= g1 );
A6:
for
n being
Element of
NAT ex
r1 being
Element of
REAL st
S1[
n,
r1]
consider s being
Real_Sequence such that A8:
for
n being
Element of
NAT holds
S1[
n,
s . n]
from FUNCT_2:sch 3(A6);
A9:
rng s c= (dom f) \ {x0}
by A8, Th2;
A10:
lim s = x0
by A8, Th2;
A11:
s is
convergent
by A8, Th2;
then A12:
lim (f /* s) = g
by A3, A10, A9;
f /* s is
convergent
by A3, A11, A10, A9;
then consider n being
Nat such that A13:
for
k being
Nat st
n <= k holds
|.(((f /* s) . k) - g).| < g1
by A4, A12, SEQ_2:def 7;
A14:
|.(((f /* s) . n) - g).| < g1
by A13;
A15:
n in NAT
by ORDINAL1:def 12;
rng s c= dom f
by A8, Th2;
then
|.((f . (s . n)) - g).| < g1
by A14, FUNCT_2:108, A15;
hence
contradiction
by A8, A15;
verum
end;
assume A16:
for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f )
; ( for g being Real ex g1 being Real st
( 0 < g1 & ( for g2 being Real holds
( not 0 < g2 or ex r1 being Real st
( 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f & not |.((f . r1) - g).| < g1 ) ) ) ) or f is_convergent_in x0 )
given g being Real such that A17:
for g1 being Real st 0 < g1 holds
ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f holds
|.((f . r1) - g).| < g1 ) )
; f is_convergent_in x0
now for s being Real_Sequence st s is convergent & lim s = x0 & rng s c= (dom f) \ {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) \ {x0} implies ( f /* s is convergent & lim (f /* s) = g ) )assume that A18:
s is
convergent
and A19:
lim s = x0
and A20:
rng s c= (dom f) \ {x0}
;
( f /* s is convergent & lim (f /* s) = g )A21:
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 A22:
0 < g1
;
ex n being Nat st
for k being Nat st n <= k holds
|.(((f /* s) . k) - g).| < g1consider g2 being
Real such that A23:
0 < g2
and A24:
for
r1 being
Real st
0 < |.(x0 - r1).| &
|.(x0 - r1).| < g2 &
r1 in dom f holds
|.((f . r1) - g).| < g1
by A17, A22;
consider n being
Element of
NAT such that A25:
for
k being
Element of
NAT st
n <= k holds
(
0 < |.(x0 - (s . k)).| &
|.(x0 - (s . k)).| < g2 &
s . k in dom f )
by A18, A19, A20, A23, Th3;
reconsider n =
n as
Nat ;
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 )A26:
k in NAT
by ORDINAL1:def 12;
assume A27:
n <= k
;
|.(((f /* s) . k) - g).| < g1then A28:
|.(x0 - (s . k)).| < g2
by A25, A26;
A29:
s . k in dom f
by A25, A27, A26;
0 < |.(x0 - (s . k)).|
by A25, A27, A26;
then
|.((f . (s . k)) - g).| < g1
by A24, A28, A29;
hence
|.(((f /* s) . k) - g).| < g1
by A20, FUNCT_2:108, XBOOLE_1:1, A26;
verum end; hence
f /* s is
convergent
by SEQ_2:def 6;
lim (f /* s) = ghence
lim (f /* s) = g
by A21, SEQ_2:def 7;
verum end;
hence
f is_convergent_in x0
by A16; verum