:: The Limit of a Composition of Real Functions
:: by Jaros{\l}aw Kotowicz
::
:: Received September 5, 1990
:: Copyright (c) 1990 Association of Mizar Users
Lm1:
for g, r being Real st 0 < g holds
( r - g < r & r < r + g )
Lm2:
for f2, f1 being PartFunc of REAL , REAL
for s being Real_Sequence st rng s c= dom (f2 * f1) holds
( rng s c= dom f1 & rng (f1 /* s) c= dom f2 )
theorem Th1: :: LIMFUNC4:1
theorem Th2: :: LIMFUNC4:2
theorem :: LIMFUNC4:3
theorem :: LIMFUNC4:4
theorem :: LIMFUNC4:5
theorem :: LIMFUNC4:6
theorem :: LIMFUNC4:7
theorem :: LIMFUNC4:8
theorem :: LIMFUNC4:9
theorem :: LIMFUNC4:10
theorem :: LIMFUNC4:11
theorem :: LIMFUNC4:12
theorem :: LIMFUNC4:13
theorem :: LIMFUNC4:14
theorem :: LIMFUNC4:15
theorem :: LIMFUNC4:16
theorem :: LIMFUNC4:17
theorem :: LIMFUNC4:18
theorem :: LIMFUNC4:19
theorem :: LIMFUNC4:20
theorem :: LIMFUNC4:21
theorem :: LIMFUNC4:22
theorem :: LIMFUNC4:23
theorem :: LIMFUNC4:24
theorem :: LIMFUNC4:25
theorem :: LIMFUNC4:26
theorem :: LIMFUNC4:27
theorem :: LIMFUNC4:28
theorem :: LIMFUNC4:29
theorem :: LIMFUNC4:30
theorem :: LIMFUNC4:31
theorem :: LIMFUNC4:32
theorem :: LIMFUNC4:33
theorem :: LIMFUNC4:34
theorem :: LIMFUNC4:35
theorem :: LIMFUNC4:36
theorem :: LIMFUNC4:37
theorem :: LIMFUNC4:38
theorem :: LIMFUNC4:39
theorem :: LIMFUNC4:40
theorem :: LIMFUNC4:41
theorem :: LIMFUNC4:42
theorem :: LIMFUNC4:43
theorem :: LIMFUNC4:44
theorem :: LIMFUNC4:45
theorem :: LIMFUNC4:46
theorem :: LIMFUNC4:47
theorem :: LIMFUNC4:48
theorem :: LIMFUNC4:49
theorem :: LIMFUNC4:50
theorem :: LIMFUNC4:51
theorem :: LIMFUNC4:52
theorem :: LIMFUNC4:53
theorem :: LIMFUNC4:54
theorem :: LIMFUNC4:55
theorem :: LIMFUNC4:56
theorem :: LIMFUNC4:57
theorem :: LIMFUNC4:58
theorem :: LIMFUNC4:59
theorem :: LIMFUNC4:60
theorem :: LIMFUNC4:61
theorem :: LIMFUNC4:62
theorem :: LIMFUNC4:63
theorem :: LIMFUNC4:64
theorem :: LIMFUNC4:65
theorem :: LIMFUNC4:66
theorem :: LIMFUNC4:67
theorem :: LIMFUNC4:68
theorem :: LIMFUNC4:69
theorem :: LIMFUNC4:70
theorem :: LIMFUNC4:71
theorem :: LIMFUNC4:72
theorem :: LIMFUNC4:73
for
x0 being
Real for
f1,
f2 being
PartFunc of
REAL ,
REAL st
f1 is_convergent_in x0 &
f2 is_left_convergent_in lim f1,
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 (f2 * f1) &
g2 < r2 &
x0 < g2 &
g2 in dom (f2 * f1) ) ) & ex
g being
Real st
(
0 < g & ( for
r being
Real st
r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds
f1 . r < lim f1,
x0 ) ) holds
(
f2 * f1 is_convergent_in x0 &
lim (f2 * f1),
x0 = lim_left f2,
(lim f1,x0) )
theorem :: LIMFUNC4:74
theorem :: LIMFUNC4:75
for
x0 being
Real for
f1,
f2 being
PartFunc of
REAL ,
REAL st
f1 is_convergent_in x0 &
f2 is_right_convergent_in lim f1,
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 (f2 * f1) &
g2 < r2 &
x0 < g2 &
g2 in dom (f2 * f1) ) ) & ex
g being
Real st
(
0 < g & ( for
r being
Real st
r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds
lim f1,
x0 < f1 . r ) ) holds
(
f2 * f1 is_convergent_in x0 &
lim (f2 * f1),
x0 = lim_right f2,
(lim f1,x0) )
theorem :: LIMFUNC4:76
theorem :: LIMFUNC4:77
for
x0 being
Real for
f1,
f2 being
PartFunc of
REAL ,
REAL st
f1 is_convergent_in x0 &
f2 is_convergent_in lim f1,
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 (f2 * f1) &
g2 < r2 &
x0 < g2 &
g2 in dom (f2 * f1) ) ) & ex
g being
Real st
(
0 < g & ( for
r being
Real st
r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds
f1 . r <> lim f1,
x0 ) ) holds
(
f2 * f1 is_convergent_in x0 &
lim (f2 * f1),
x0 = lim f2,
(lim f1,x0) )