let f1, f2 be PartFunc of REAL,REAL; ( f1 is convergent_in-infty & f2 is convergent_in-infty & ex r being Real st
( ( (dom f1) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) & ( for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & ( for g being Real st g in (dom f2) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) ) implies lim_in-infty f1 <= lim_in-infty f2 )
assume that
A1:
f1 is convergent_in-infty
and
A2:
f2 is convergent_in-infty
; ( for r being Real holds
( not ( (dom f1) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) & ( for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) & not ( (dom f2) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & ( for g being Real st g in (dom f2) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) ) or lim_in-infty f1 <= lim_in-infty f2 )
given r being Real such that A3:
( ( (dom f1) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) & ( for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & ( for g being Real st g in (dom f2) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) )
; lim_in-infty f1 <= lim_in-infty f2
now lim_in-infty f1 <= lim_in-infty f2per cases
( ( (dom f1) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) & ( for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & ( for g being Real st g in (dom f2) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) )
by A3;
suppose A4:
(
(dom f1) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) & ( for
g being
Real st
g in (dom f1) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) )
;
lim_in-infty f1 <= lim_in-infty f2deffunc H1(
Nat)
-> object =
- $1;
defpred S1[
Nat,
Real]
means ( $2
< - $1 & $2
in (dom f1) /\ (left_open_halfline r) );
consider s1 being
Real_Sequence such that A5:
for
n being
Nat holds
s1 . n = H1(
n)
from SEQ_1:sch 1();
consider s2 being
Real_Sequence such that A10:
for
n being
Element of
NAT holds
S1[
n,
s2 . n]
from FUNCT_2:sch 3(A6);
then A11:
s2 is
divergent_to-infty
by A5, Th21, Th43;
A12:
rng s2 c= dom f2
then A13:
lim (f2 /* s2) = lim_in-infty f2
by A2, A11, Def13;
A14:
rng s2 c= dom f1
A17:
f2 /* s2 is
convergent
by A2, A11, A12;
A18:
f1 /* s2 is
convergent
by A1, A11, A14;
lim (f1 /* s2) = lim_in-infty f1
by A1, A11, A14, Def13;
hence
lim_in-infty f1 <= lim_in-infty f2
by A18, A17, A13, A15, SEQ_2:18;
verum end; suppose A19:
(
(dom f2) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & ( for
g being
Real st
g in (dom f2) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) )
;
lim_in-infty f1 <= lim_in-infty f2deffunc H1(
Nat)
-> object =
- $1;
defpred S1[
Nat,
Real]
means ( $2
< - $1 & $2
in (dom f2) /\ (left_open_halfline r) );
consider s1 being
Real_Sequence such that A20:
for
n being
Nat holds
s1 . n = H1(
n)
from SEQ_1:sch 1();
consider s2 being
Real_Sequence such that A25:
for
n being
Element of
NAT holds
S1[
n,
s2 . n]
from FUNCT_2:sch 3(A21);
then A26:
s2 is
divergent_to-infty
by A20, Th21, Th43;
A27:
rng s2 c= dom f1
then A28:
lim (f1 /* s2) = lim_in-infty f1
by A1, A26, Def13;
A29:
rng s2 c= dom f2
A32:
f1 /* s2 is
convergent
by A1, A26, A27;
A33:
f2 /* s2 is
convergent
by A2, A26, A29;
lim (f2 /* s2) = lim_in-infty f2
by A2, A26, A29, Def13;
hence
lim_in-infty f1 <= lim_in-infty f2
by A33, A32, A28, A30, SEQ_2:18;
verum end; end; end;
hence
lim_in-infty f1 <= lim_in-infty f2
; verum