begin
Lm1:
for g, r, 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 set st rng seq c= (dom (f1 (#) f2)) \ X holds
( rng seq c= dom (f1 (#) f2) & 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 set st rng seq c= (dom (f1 + f2)) \ X holds
( rng seq c= dom (f1 + f2) & 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 )
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
for
x0 being
Real for
f being
PartFunc of
REAL,
REAL holds
( ( for
r1,
r2 being
Real st
r1 < x0 &
x0 < r2 holds
ex
g1,
g2 being
Real st
(
r1 < g1 &
g1 < x0 &
g1 in dom f &
g2 < r2 &
x0 < g2 &
g2 in dom f ) ) iff ( ( for
r being
Real st
r < x0 holds
ex
g being
Real st
(
r < g &
g < x0 &
g in dom f ) ) & ( for
r being
Real st
x0 < r holds
ex
g being
Real st
(
g < r &
x0 < g &
g in dom f ) ) ) )
:: deftheorem Def1 defines is_convergent_in LIMFUNC3:def 1 :
for f being PartFunc of REAL,REAL
for x0 being Real holds
( f is_convergent_in x0 iff ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ex g being Real st
for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds
( f /* seq is convergent & lim (f /* seq) = g ) ) );
:: deftheorem Def2 defines is_divergent_to+infty_in LIMFUNC3:def 2 :
for f being PartFunc of REAL,REAL
for x0 being Real holds
( f is_divergent_to+infty_in x0 iff ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds
f /* seq is divergent_to+infty ) ) );
:: deftheorem Def3 defines is_divergent_to-infty_in LIMFUNC3:def 3 :
for f being PartFunc of REAL,REAL
for x0 being Real holds
( f is_divergent_to-infty_in x0 iff ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ( for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds
f /* seq is divergent_to-infty ) ) );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem Th15:
theorem Th16:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th23:
theorem
theorem Th25:
theorem
theorem Th27:
for
x0 being
Real for
f1,
f being
PartFunc of
REAL,
REAL st
f1 is_divergent_to+infty_in x0 & ( for
r1,
r2 being
Real st
r1 < x0 &
x0 < r2 holds
ex
g1,
g2 being
Real st
(
r1 < g1 &
g1 < x0 &
g1 in dom f &
g2 < r2 &
x0 < g2 &
g2 in dom f ) ) & ex
r being
Real st
(
0 < r &
(dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & ( for
g being
Real st
g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
f1 . g <= f . g ) ) holds
f is_divergent_to+infty_in x0
theorem Th28:
for
x0 being
Real for
f1,
f being
PartFunc of
REAL,
REAL st
f1 is_divergent_to-infty_in x0 & ( for
r1,
r2 being
Real st
r1 < x0 &
x0 < r2 holds
ex
g1,
g2 being
Real st
(
r1 < g1 &
g1 < x0 &
g1 in dom f &
g2 < r2 &
x0 < g2 &
g2 in dom f ) ) & ex
r being
Real st
(
0 < r &
(dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & ( for
g being
Real st
g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
f . g <= f1 . g ) ) holds
f is_divergent_to-infty_in x0
theorem
theorem
:: deftheorem Def4 defines lim LIMFUNC3:def 4 :
for f being PartFunc of REAL,REAL
for x0 being Real st f is_convergent_in x0 holds
for b3 being Real holds
( b3 = lim (f,x0) iff for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds
( f /* seq is convergent & lim (f /* seq) = b3 ) );
theorem
canceled;
theorem
theorem Th33:
theorem
theorem Th35:
theorem Th36:
theorem Th37:
theorem
theorem
theorem
theorem Th41:
theorem Th42:
theorem
theorem
theorem Th45:
for
x0 being
Real for
f1,
f2,
f being
PartFunc of
REAL,
REAL st
f1 is_convergent_in x0 &
f2 is_convergent_in x0 &
lim (
f1,
x0)
= lim (
f2,
x0) & ( for
r1,
r2 being
Real st
r1 < x0 &
x0 < r2 holds
ex
g1,
g2 being
Real st
(
r1 < g1 &
g1 < x0 &
g1 in dom f &
g2 < r2 &
x0 < g2 &
g2 in dom f ) ) & ex
r being
Real st
(
0 < r & ( for
g being
Real st
g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
(
f1 . g <= f . g &
f . g <= f2 . g ) ) & ( (
(dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) &
(dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) ) or (
(dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) &
(dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) ) ) ) holds
(
f is_convergent_in x0 &
lim (
f,
x0)
= lim (
f1,
x0) )
theorem
for
x0 being
Real for
f1,
f2,
f being
PartFunc of
REAL,
REAL st
f1 is_convergent_in x0 &
f2 is_convergent_in x0 &
lim (
f1,
x0)
= lim (
f2,
x0) & ex
r being
Real st
(
0 < r &
].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for
g being
Real st
g in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ holds
(
f1 . g <= f . g &
f . g <= f2 . g ) ) ) holds
(
f is_convergent_in x0 &
lim (
f,
x0)
= lim (
f1,
x0) )
theorem
for
x0 being
Real for
f1,
f2 being
PartFunc of
REAL,
REAL st
f1 is_convergent_in x0 &
f2 is_convergent_in x0 & ex
r being
Real st
(
0 < r & ( (
(dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & ( for
g being
Real st
g in (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
f1 . g <= f2 . g ) ) or (
(dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & ( for
g being
Real st
g in (dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
f1 . g <= f2 . g ) ) ) ) holds
lim (
f1,
x0)
<= lim (
f2,
x0)
theorem
theorem
theorem
theorem
theorem