let x0 be Real; for f being PartFunc of REAL,REAL holds
( f is_left_divergent_to-infty_in x0 iff ( ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ) & ( for g1 being Real ex r being Real st
( r < x0 & ( for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds
f . r1 < g1 ) ) ) ) )
let f be PartFunc of REAL,REAL; ( f is_left_divergent_to-infty_in x0 iff ( ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ) & ( for g1 being Real ex r being Real st
( r < x0 & ( for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds
f . r1 < g1 ) ) ) ) )
thus
( f is_left_divergent_to-infty_in x0 implies ( ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ) & ( for g1 being Real ex r being Real st
( r < x0 & ( for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds
f . r1 < g1 ) ) ) ) )
( ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ) & ( for g1 being Real ex r being Real st
( r < x0 & ( for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds
f . r1 < g1 ) ) ) implies f is_left_divergent_to-infty_in x0 )proof
assume that A1:
f is_left_divergent_to-infty_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 ex
g1 being
Real st
for
r being
Real st
r < x0 holds
ex
r1 being
Real st
(
r < r1 &
r1 < x0 &
r1 in dom f &
g1 <= f . r1 ) )
;
contradiction
consider g1 being
Real such that A3:
for
r being
Real st
r < x0 holds
ex
r1 being
Real st
(
r < r1 &
r1 < x0 &
r1 in dom f &
g1 <= f . r1 )
by A1, A2;
defpred S1[
Nat,
Real]
means (
x0 - (1 / ($1 + 1)) < $2 & $2
< x0 & $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) /\ (left_open_halfline x0)
by A10, Th5;
A12:
lim s = x0
by A10, Th5;
s is
convergent
by A10, Th5;
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, Th5;
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 r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f )
and
A17:
for g1 being Real ex r being Real st
( r < x0 & ( for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds
f . r1 < g1 ) )
; f is_left_divergent_to-infty_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 divergent_to-infty let s be
Real_Sequence;
( s is convergent & lim s = x0 & rng s c= (dom f) /\ (left_open_halfline x0) implies f /* s is divergent_to-infty )assume that A18:
s is
convergent
and A19:
lim s = x0
and A20:
rng s c= (dom f) /\ (left_open_halfline x0)
;
f /* s is divergent_to-infty A21:
(dom f) /\ (left_open_halfline x0) c= dom f
by XBOOLE_1:17;
now for g1 being Real ex n being Nat st
for k being Nat st n <= k holds
(f /* s) . k < g1let g1 be
Real;
ex n being Nat st
for k being Nat st n <= k holds
(f /* s) . k < g1consider r being
Real such that A22:
r < x0
and A23:
for
r1 being
Real st
r < r1 &
r1 < x0 &
r1 in dom f holds
f . r1 < g1
by A17;
consider n being
Nat such that A24:
for
k being
Nat st
n <= k holds
r < s . k
by A18, A19, A22, Th1;
take n =
n;
for k being Nat st n <= k holds
(f /* s) . k < g1let k be
Nat;
( n <= k implies (f /* s) . k < g1 )assume A25:
n <= k
;
(f /* s) . k < g1A26:
s . k in rng s
by VALUED_0:28;
then
s . k in left_open_halfline x0
by A20, XBOOLE_0:def 4;
then
s . k in { g2 where g2 is Real : g2 < x0 }
by XXREAL_1:229;
then A27:
ex
g2 being
Real st
(
g2 = s . k &
g2 < x0 )
;
A28:
k in NAT
by ORDINAL1:def 12;
s . k in dom f
by A20, A26, XBOOLE_0:def 4;
then
f . (s . k) < g1
by A23, A24, A25, A27;
hence
(f /* s) . k < g1
by A20, A21, FUNCT_2:108, XBOOLE_1:1, A28;
verum end; hence
f /* s is
divergent_to-infty
;
verum end;
hence
f is_left_divergent_to-infty_in x0
by A16; verum