begin
Lm1:
for r, g, r1 being real number st 0 < g & r <= r1 holds
( r - g < r1 & r < r1 + g )
Lm2:
for seq being Real_Sequence
for f1, f2 being PartFunc of REAL,REAL
for X being Subset of REAL st rng seq c= (dom (f1 (#) f2)) /\ X holds
( rng seq c= dom (f1 (#) f2) & rng seq c= X & dom (f1 (#) f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= dom f2 & rng seq c= (dom f1) /\ X & rng seq c= (dom f2) /\ X )
Lm3:
for r being Real
for n being Element of NAT holds
( r - (1 / (n + 1)) < r & r < r + (1 / (n + 1)) )
Lm4:
for seq being Real_Sequence
for f1, f2 being PartFunc of REAL,REAL
for X being Subset of REAL st rng seq c= (dom (f1 + f2)) /\ X holds
( rng seq c= dom (f1 + f2) & rng seq c= X & dom (f1 + f2) = (dom f1) /\ (dom f2) & rng seq c= (dom f1) /\ X & rng seq c= (dom f2) /\ X )
Lm5:
for x0 being Real
for seq being Real_Sequence
for f being PartFunc of REAL,REAL st ( 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 ) ) ) & seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) holds
f /* seq is divergent_to-infty
theorem Th63:
for
x0 being
Real for
f1,
f2,
f being
PartFunc of
REAL,
REAL st
f1 is_left_convergent_in x0 &
f2 is_left_convergent_in x0 &
lim_left (
f1,
x0)
= lim_left (
f2,
x0) & ( for
r being
Real st
r < x0 holds
ex
g being
Real st
(
r < g &
g < x0 &
g in dom f ) ) & ex
r being
Real st
(
0 < r & ( for
g being
Real st
g in (dom f) /\ ].(x0 - r),x0.[ holds
(
f1 . g <= f . g &
f . g <= f2 . g ) ) & ( (
(dom f1) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ &
(dom f) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ ) or (
(dom f2) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ &
(dom f) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ ) ) ) holds
(
f is_left_convergent_in x0 &
lim_left (
f,
x0)
= lim_left (
f1,
x0) )
theorem Th65:
for
x0 being
Real for
f1,
f2,
f being
PartFunc of
REAL,
REAL st
f1 is_right_convergent_in x0 &
f2 is_right_convergent_in x0 &
lim_right (
f1,
x0)
= lim_right (
f2,
x0) & ( for
r being
Real st
x0 < r holds
ex
g being
Real st
(
g < r &
x0 < g &
g in dom f ) ) & ex
r being
Real st
(
0 < r & ( for
g being
Real st
g in (dom f) /\ ].x0,(x0 + r).[ holds
(
f1 . g <= f . g &
f . g <= f2 . g ) ) & ( (
(dom f1) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ &
(dom f) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ ) or (
(dom f2) /\ ].x0,(x0 + r).[ c= (dom f1) /\ ].x0,(x0 + r).[ &
(dom f) /\ ].x0,(x0 + r).[ c= (dom f2) /\ ].x0,(x0 + r).[ ) ) ) holds
(
f is_right_convergent_in x0 &
lim_right (
f,
x0)
= lim_right (
f1,
x0) )
theorem
for
x0 being
Real for
f1,
f2 being
PartFunc of
REAL,
REAL st
f1 is_left_convergent_in x0 &
f2 is_left_convergent_in x0 & ex
r being
Real st
(
0 < r & ( (
(dom f1) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ & ( for
g being
Real st
g in (dom f1) /\ ].(x0 - r),x0.[ holds
f1 . g <= f2 . g ) ) or (
(dom f2) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ & ( for
g being
Real st
g in (dom f2) /\ ].(x0 - r),x0.[ holds
f1 . g <= f2 . g ) ) ) ) holds
lim_left (
f1,
x0)
<= lim_left (
f2,
x0)
theorem
for
x0 being
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)