let x0 be Real; for f being PartFunc of REAL,REAL holds
( f is_divergent_to+infty_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 ) ) & ( for g1 being Real ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f holds
g1 < f . r1 ) ) ) ) )
let f be PartFunc of REAL,REAL; ( f is_divergent_to+infty_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 ) ) & ( for g1 being Real ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f holds
g1 < f . r1 ) ) ) ) )
thus
( f is_divergent_to+infty_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 ) ) & ( for g1 being Real ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f holds
g1 < f . r1 ) ) ) ) )
( ( 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 g1 being Real ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f holds
g1 < f . r1 ) ) ) implies f is_divergent_to+infty_in x0 )proof
assume that A1:
f is_divergent_to+infty_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 ex
g1 being
Real st
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 <= g1 ) )
;
contradiction
consider g1 being
Real such that A3:
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 <= 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
<= g1 );
A4:
for
n being
Element of
NAT ex
r1 being
Element of
REAL st
S1[
n,
r1]
consider s being
Real_Sequence such that A6:
for
n being
Element of
NAT holds
S1[
n,
s . n]
from FUNCT_2:sch 3(A4);
A7:
rng s c= (dom f) \ {x0}
by A6, Th2;
A8:
lim s = x0
by A6, Th2;
s is
convergent
by A6, Th2;
then
f /* s is
divergent_to+infty
by A1, A8, A7;
then consider n being
Nat such that A9:
for
k being
Nat st
n <= k holds
g1 < (f /* s) . k
;
A10:
g1 < (f /* s) . n
by A9;
A11:
n in NAT
by ORDINAL1:def 12;
rng s c= dom f
by A6, Th2;
then
g1 < f . (s . n)
by A10, FUNCT_2:108, A11;
hence
contradiction
by A6, A11;
verum
end;
assume that
A12:
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 )
and
A13:
for g1 being Real ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f holds
g1 < f . r1 ) )
; f is_divergent_to+infty_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 divergent_to+infty let s be
Real_Sequence;
( s is convergent & lim s = x0 & rng s c= (dom f) \ {x0} implies f /* s is divergent_to+infty )assume that A14:
s is
convergent
and A15:
lim s = x0
and A16:
rng s c= (dom f) \ {x0}
;
f /* s is divergent_to+infty now for g1 being Real ex n being Nat st
for k being Nat st n <= k holds
g1 < (f /* s) . klet g1 be
Real;
ex n being Nat st
for k being Nat st n <= k holds
g1 < (f /* s) . kconsider g2 being
Real such that A17:
0 < g2
and A18:
for
r1 being
Real st
0 < |.(x0 - r1).| &
|.(x0 - r1).| < g2 &
r1 in dom f holds
g1 < f . r1
by A13;
consider n being
Element of
NAT such that A19:
for
k being
Element of
NAT st
n <= k holds
(
0 < |.(x0 - (s . k)).| &
|.(x0 - (s . k)).| < g2 &
s . k in dom f )
by A14, A15, A16, A17, Th3;
reconsider n =
n as
Nat ;
take n =
n;
for k being Nat st n <= k holds
g1 < (f /* s) . klet k be
Nat;
( n <= k implies g1 < (f /* s) . k )A20:
k in NAT
by ORDINAL1:def 12;
assume A21:
n <= k
;
g1 < (f /* s) . kthen A22:
|.(x0 - (s . k)).| < g2
by A19, A20;
A23:
s . k in dom f
by A19, A21, A20;
0 < |.(x0 - (s . k)).|
by A19, A21, A20;
then
g1 < f . (s . k)
by A18, A22, A23;
hence
g1 < (f /* s) . k
by A16, FUNCT_2:108, XBOOLE_1:1, A20;
verum end; hence
f /* s is
divergent_to+infty
;
verum end;
hence
f is_divergent_to+infty_in x0
by A12; verum