let x0 be Real; for f being PartFunc of REAL,REAL holds
( f is_right_divergent_to-infty_in x0 iff ( ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ) & ( for g1 being Real ex r being Real st
( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
f . r1 < g1 ) ) ) ) )
let f be PartFunc of REAL,REAL; ( f is_right_divergent_to-infty_in x0 iff ( ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ) & ( for g1 being Real ex r being Real st
( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
f . r1 < g1 ) ) ) ) )
thus
( f is_right_divergent_to-infty_in x0 implies ( ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ) & ( for g1 being Real ex r being Real st
( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
f . r1 < g1 ) ) ) ) )
( ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ) & ( for g1 being Real ex r being Real st
( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
f . r1 < g1 ) ) ) implies f is_right_divergent_to-infty_in x0 )proof
assume that A1:
f is_right_divergent_to-infty_in x0
and A2:
( ex
r being
Real st
(
x0 < r & ( for
g being
Real holds
( not
g < r or not
x0 < g or not
g in dom f ) ) ) or ex
g1 being
Real st
for
r being
Real st
x0 < r holds
ex
r1 being
Real st
(
r1 < r &
x0 < r1 &
r1 in dom f &
g1 <= f . r1 ) )
;
contradiction
consider g1 being
Real such that A3:
for
r being
Real st
x0 < r holds
ex
r1 being
Real st
(
r1 < r &
x0 < r1 &
r1 in dom f &
g1 <= f . r1 )
by A1, A2;
defpred S1[
Nat,
Real]
means (
x0 < $2 & $2
< x0 + (1 / ($1 + 1)) & $2
in dom f &
g1 <= f . $2 );
consider s being
Real_Sequence such that A9:
for
n being
Element of
NAT holds
S1[
n,
s . n]
from FUNCT_2:sch 3(A4);
A10:
for
n being
Nat holds
S1[
n,
s . n]
A11:
rng s c= (dom f) /\ (right_open_halfline x0)
by A10, Th6;
A12:
lim s = x0
by A10, Th6;
s is
convergent
by A10, Th6;
then
f /* s is
divergent_to-infty
by A1, A12, A11;
then consider n being
Nat such that A13:
for
k being
Nat st
n <= k holds
(f /* s) . k < g1
;
A14:
(f /* s) . n < g1
by A13;
A15:
n in NAT
by ORDINAL1:def 12;
rng s c= dom f
by A10, Th6;
then
f . (s . n) < g1
by A14, FUNCT_2:108, A15;
hence
contradiction
by A10;
verum
end;
assume that
A16:
for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f )
and
A17:
for g1 being Real ex r being Real st
( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
f . r1 < g1 ) )
; f is_right_divergent_to-infty_in x0
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 divergent_to-infty
by A17, Lm5;
hence
f is_right_divergent_to-infty_in x0
by A16; verum