let x0 be Real; for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & ex r being Real st
( 0 < r & ( ( (dom f1) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f1) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f2) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) ) ) ) holds
lim_right (f1,x0) <= lim_right (f2,x0)
let f1, f2 be PartFunc of REAL,REAL; ( f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & ex r being Real st
( 0 < r & ( ( (dom f1) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f1) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f2) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) ) ) ) implies lim_right (f1,x0) <= lim_right (f2,x0) )
assume that
A1:
f1 is_right_convergent_in x0
and
A2:
f2 is_right_convergent_in x0
; ( for r being Real holds
( not 0 < r or ( not ( (dom f1) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f1) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) ) & not ( (dom f2) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f2) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) ) ) ) or lim_right (f1,x0) <= lim_right (f2,x0) )
given r being Real such that A3:
0 < r
and
A4:
( ( (dom f1) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f1) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f2) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) ) )
; lim_right (f1,x0) <= lim_right (f2,x0)
now lim_right (f1,x0) <= lim_right (f2,x0)per cases
( ( (dom f1) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f1) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & ( for g being Real st g in (dom f2) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) ) )
by A4;
suppose A5:
(
(dom f1) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ & ( for
g being
Real st
g in (dom f1) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) )
;
lim_right (f1,x0) <= lim_right (f2,x0)defpred S1[
Nat,
Real]
means (
x0 < $2 & $2
< x0 + (1 / ($1 + 1)) & $2
in dom f1 );
consider s being
Real_Sequence such that A10:
for
n being
Element of
NAT holds
S1[
n,
s . n]
from FUNCT_2:sch 3(A6);
A11:
for
n being
Nat holds
S1[
n,
s . n]
A12:
lim s = x0
by A11, Th6;
A13:
rng s c= (dom f1) /\ (right_open_halfline x0)
by A11, Th6;
A14:
].x0,(x0 + r).[ c= right_open_halfline x0
by XXREAL_1:247;
A15:
s is
convergent
by A11, Th6;
x0 < x0 + r
by A3, Lm1;
then consider k being
Nat such that A16:
for
n being
Nat st
k <= n holds
s . n < x0 + r
by A15, A12, Th2;
A17:
lim (s ^\ k) = x0
by A15, A12, SEQ_4:20;
then A21:
rng (s ^\ k) c= (dom f1) /\ ].x0,(x0 + r).[
by TARSKI:def 3;
then A22:
rng (s ^\ k) c= (dom f2) /\ ].x0,(x0 + r).[
by A5, XBOOLE_1:1;
(dom f2) /\ ].x0,(x0 + r).[ c= ].x0,(x0 + r).[
by XBOOLE_1:17;
then
rng (s ^\ k) c= ].x0,(x0 + r).[
by A22, XBOOLE_1:1;
then A23:
rng (s ^\ k) c= right_open_halfline x0
by A14, XBOOLE_1:1;
A24:
(dom f2) /\ ].x0,(x0 + r).[ c= dom f2
by XBOOLE_1:17;
then
rng (s ^\ k) c= dom f2
by A22, XBOOLE_1:1;
then A25:
rng (s ^\ k) c= (dom f2) /\ (right_open_halfline x0)
by A23, XBOOLE_1:19;
then A26:
lim (f2 /* (s ^\ k)) = lim_right (
f2,
x0)
by A2, A15, A17, Def8;
rng (s ^\ k) c= rng s
by VALUED_0:21;
then A27:
rng (s ^\ k) c= (dom f1) /\ (right_open_halfline x0)
by A13, XBOOLE_1:1;
then A28:
lim (f1 /* (s ^\ k)) = lim_right (
f1,
x0)
by A1, A15, A17, Def8;
A29:
(dom f1) /\ ].x0,(x0 + r).[ c= dom f1
by XBOOLE_1:17;
A32:
f2 /* (s ^\ k) is
convergent
by A2, A15, A17, A25;
f1 /* (s ^\ k) is
convergent
by A1, A15, A17, A27;
hence
lim_right (
f1,
x0)
<= lim_right (
f2,
x0)
by A28, A32, A26, A30, SEQ_2:18;
verum end; suppose A33:
(
(dom f2) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ & ( for
g being
Real st
g in (dom f2) /\ ].x0,(x0 + r).[ holds
f1 . g <= f2 . g ) )
;
lim_right (f1,x0) <= lim_right (f2,x0)defpred S1[
Nat,
Real]
means (
x0 < $2 & $2
< x0 + (1 / ($1 + 1)) & $2
in dom f2 );
consider s being
Real_Sequence such that A38:
for
n being
Element of
NAT holds
S1[
n,
s . n]
from FUNCT_2:sch 3(A34);
A39:
for
n being
Nat holds
S1[
n,
s . n]
A40:
lim s = x0
by A39, Th6;
A41:
rng s c= (dom f2) /\ (right_open_halfline x0)
by A39, Th6;
A42:
].x0,(x0 + r).[ c= right_open_halfline x0
by XXREAL_1:247;
A43:
s is
convergent
by A39, Th6;
x0 < x0 + r
by A3, Lm1;
then consider k being
Nat such that A44:
for
n being
Nat st
k <= n holds
s . n < x0 + r
by A43, A40, Th2;
A45:
lim (s ^\ k) = x0
by A43, A40, SEQ_4:20;
then A50:
rng (s ^\ k) c= (dom f2) /\ ].x0,(x0 + r).[
by TARSKI:def 3;
then A51:
rng (s ^\ k) c= (dom f1) /\ ].x0,(x0 + r).[
by A33, XBOOLE_1:1;
(dom f1) /\ ].x0,(x0 + r).[ c= ].x0,(x0 + r).[
by XBOOLE_1:17;
then
rng (s ^\ k) c= ].x0,(x0 + r).[
by A51, XBOOLE_1:1;
then A52:
rng (s ^\ k) c= right_open_halfline x0
by A42, XBOOLE_1:1;
A53:
(dom f1) /\ ].x0,(x0 + r).[ c= dom f1
by XBOOLE_1:17;
then
rng (s ^\ k) c= dom f1
by A51, XBOOLE_1:1;
then A54:
rng (s ^\ k) c= (dom f1) /\ (right_open_halfline x0)
by A52, XBOOLE_1:19;
then A55:
lim (f1 /* (s ^\ k)) = lim_right (
f1,
x0)
by A1, A43, A45, Def8;
rng (s ^\ k) c= rng s
by VALUED_0:21;
then A56:
rng (s ^\ k) c= (dom f2) /\ (right_open_halfline x0)
by A41, XBOOLE_1:1;
then A57:
lim (f2 /* (s ^\ k)) = lim_right (
f2,
x0)
by A2, A43, A45, Def8;
A58:
(dom f2) /\ ].x0,(x0 + r).[ c= dom f2
by XBOOLE_1:17;
A61:
f1 /* (s ^\ k) is
convergent
by A1, A43, A45, A54;
f2 /* (s ^\ k) is
convergent
by A2, A43, A45, A56;
hence
lim_right (
f1,
x0)
<= lim_right (
f2,
x0)
by A57, A61, A55, A59, SEQ_2:18;
verum end; end; end;
hence
lim_right (f1,x0) <= lim_right (f2,x0)
; verum