environ
vocabularies HIDDEN, PARTFUN1, NUMBERS, REAL_1, SEQ_1, SUBSET_1, FCONT_1, ARYTM_3, RELAT_1, LIMFUNC3, SEQ_2, ORDINAL2, TARSKI, XBOOLE_0, FUNCT_2, FUNCT_1, LIMFUNC2, LIMFUNC1, RCOMP_1, CARD_1, XXREAL_1, ARYTM_1, FDIFF_1, VALUED_1, XXREAL_0, NAT_1, ASYMPT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, RELSET_1, PARTFUN1, RFUNCT_1, RCOMP_1, FCONT_1, FDIFF_1, LIMFUNC1, LIMFUNC2, LIMFUNC3, XXREAL_0;
definitions TARSKI;
theorems TARSKI, NAT_1, RFUNCT_1, RCOMP_1, FCONT_1, FDIFF_1, ROLLE, SEQ_2, SEQ_4, LIMFUNC2, LIMFUNC1, LIMFUNC3, ZFMISC_1, FUNCT_1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, XXREAL_0, VALUED_1, XXREAL_1, XXREAL_2, FUNCT_2, VALUED_0, ORDINAL1, SEQ_1;
schemes FUNCT_2;
registrations ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, RCOMP_1, VALUED_0, XXREAL_2, XBOOLE_0, SEQ_4, FUNCT_2, SEQ_1, SEQ_2;
constructors HIDDEN, PARTFUN1, FUNCOP_1, REAL_1, NAT_1, SEQ_2, SEQM_3, PROB_1, RCOMP_1, RFUNCT_1, RFUNCT_2, FCONT_1, LIMFUNC1, FDIFF_1, LIMFUNC2, LIMFUNC3, VALUED_1, XXREAL_2, RELSET_1, SEQ_4, COMSEQ_2, SEQ_1;
requirements HIDDEN, SUBSET, BOOLE, ARITHM, NUMERALS;
equalities PROB_1, LIMFUNC1;
expansions TARSKI;
theorem
for
f,
g being
PartFunc of
REAL,
REAL for
x0 being
Real st
x0 in (dom f) /\ (dom g) & ex
r being
Real st
(
r > 0 &
[.x0,(x0 + r).] c= dom f &
[.x0,(x0 + r).] c= dom g &
f is_differentiable_on ].x0,(x0 + r).[ &
g is_differentiable_on ].x0,(x0 + r).[ &
].x0,(x0 + r).[ c= dom (f / g) &
[.x0,(x0 + r).] c= dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) &
f . x0 = 0 &
g . x0 = 0 &
f is_continuous_in x0 &
g is_continuous_in x0 &
(f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[) is_right_convergent_in x0 ) holds
(
f / g is_right_convergent_in x0 & ex
r being
Real st
(
r > 0 &
lim_right (
(f / g),
x0)
= lim_right (
((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),
x0) ) )
theorem
for
f,
g being
PartFunc of
REAL,
REAL for
x0 being
Real st
x0 in (dom f) /\ (dom g) & ex
r being
Real st
(
r > 0 &
[.(x0 - r),x0.] c= dom f &
[.(x0 - r),x0.] c= dom g &
f is_differentiable_on ].(x0 - r),x0.[ &
g is_differentiable_on ].(x0 - r),x0.[ &
].(x0 - r),x0.[ c= dom (f / g) &
[.(x0 - r),x0.] c= dom ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) &
f . x0 = 0 &
g . x0 = 0 &
f is_continuous_in x0 &
g is_continuous_in x0 &
(f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[) is_left_convergent_in x0 ) holds
(
f / g is_left_convergent_in x0 & ex
r being
Real st
(
r > 0 &
lim_left (
(f / g),
x0)
= lim_left (
((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),
x0) ) )