environ
vocabularies HIDDEN, NUMBERS, REAL_1, SUBSET_1, SEQ_1, FDIFF_1, FUNCT_1, RCOMP_1, PARTFUN1, ARYTM_1, VALUED_0, SEQ_2, ORDINAL2, CARD_1, RELAT_1, ARYTM_3, XXREAL_0, COMPLEX1, NAT_1, TARSKI, VALUED_1, FUNCT_2, FUNCOP_1, XXREAL_1, FCONT_1, SQUARE_1, XBOOLE_0, ORDINAL4, LIMFUNC1, FUNCT_7, ASYMPT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, SQUARE_1, NAT_1, FUNCT_1, FUNCT_2, VALUED_0, VALUED_1, SEQ_1, RELSET_1, COMSEQ_2, SEQ_2, PARTFUN1, PARTFUN2, RFUNCT_1, RCOMP_1, FCONT_1, FDIFF_1, LIMFUNC1, RECDEF_1;
definitions TARSKI, XBOOLE_0, FDIFF_1, VALUED_1;
theorems TARSKI, FUNCT_1, FUNCT_2, NAT_1, SEQ_1, SEQ_2, SEQM_3, SEQ_4, ABSVALUE, PARTFUN1, PARTFUN2, RCOMP_1, RFUNCT_1, RFUNCT_2, FCONT_1, FDIFF_1, SCHEME1, ROLLE, FCONT_3, FUNCT_3, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, COMPLEX1, FUNCOP_1, XREAL_1, XXREAL_0, ORDINAL1, VALUED_1, XXREAL_1, VALUED_0, XREAL_0, NUMBERS;
schemes NAT_1, RECDEF_1, SEQ_1, SCHEME1, FUNCT_2;
registrations ORDINAL1, RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, MEMBERED, SEQM_3, RCOMP_1, RFUNCT_2, FDIFF_1, FCONT_3, VALUED_0, VALUED_1, FUNCT_2, SEQ_4, SQUARE_1, SEQ_1, SEQ_2;
constructors HIDDEN, PARTFUN1, REAL_1, SQUARE_1, NAT_1, COMPLEX1, SEQ_2, SEQM_3, PROB_1, RCOMP_1, PARTFUN2, RFUNCT_1, RFUNCT_2, FCONT_1, LIMFUNC1, FDIFF_1, VALUED_1, RECDEF_1, RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2, SEQ_1, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XBOOLE_0, SQUARE_1, SUBSET_1, LIMFUNC1, PROB_1, VALUED_1;
expansions TARSKI, XBOOLE_0, FDIFF_1, FUNCT_2;
Lm1:
for x0 being Real
for f being PartFunc of REAL,REAL st ex N being Neighbourhood of x0 st N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) holds
( f is_differentiable_in x0 & ( for h being non-zero 0 -convergent Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) )
Lm2:
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st ex N being Neighbourhood of x0 st N c= dom (f2 * f1) & f1 is_differentiable_in x0 & f2 is_differentiable_in f1 . x0 holds
( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) )
reconsider jj = 1 as Element of REAL by NUMBERS:19;
Lm3:
for f being PartFunc of REAL,REAL holds (f (#) f) " {0} = f " {0}
theorem
for
g,
p being
Real for
f being
one-to-one PartFunc of
REAL,
REAL st
].p,g.[ c= dom f &
f is_differentiable_on ].p,g.[ & ( for
x0 being
Real st
x0 in ].p,g.[ holds
0 < diff (
f,
x0) or for
x0 being
Real st
x0 in ].p,g.[ holds
diff (
f,
x0)
< 0 ) holds
(
f | ].p,g.[ is
one-to-one &
(f | ].p,g.[) " is_differentiable_on dom ((f | ].p,g.[) ") & ( for
x0 being
Real st
x0 in dom ((f | ].p,g.[) ") holds
diff (
((f | ].p,g.[) "),
x0)
= 1
/ (diff (f,(((f | ].p,g.[) ") . x0))) ) )