X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FRolle.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FRolle.ma;h=21e3b8c34874f1a4f89a401e4bea9189ff9de347;hb=80110e17ef1d38d71473e9471ce15beddde663bb;hp=c8e8cdc4fa23cce50ee22cc04c0a042d79b8f30d;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/Rolle.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/Rolle.ma index c8e8cdc4f..21e3b8c34 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/Rolle.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/Rolle.ma @@ -16,15 +16,13 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/Rolle". +include "CoRN.ma". + (* $Id: Rolle.v,v 1.6 2004/04/23 10:01:01 lcf Exp $ *) -(* INCLUDE -DiffTactics2 -*) +include "tactics/DiffTactics2.ma". -(* INCLUDE -MoreFunctions -*) +include "ftc/MoreFunctions.ma". (* UNEXPORTED Section Rolle. @@ -44,113 +42,113 @@ We now begin to work with partial functions. We begin by stating and proving Ro (* begin hide *) -inline cic:/CoRN/ftc/Rolle/a.var. +inline "cic:/CoRN/ftc/Rolle/a.var". -inline cic:/CoRN/ftc/Rolle/b.var. +inline "cic:/CoRN/ftc/Rolle/b.var". -inline cic:/CoRN/ftc/Rolle/Hab'.var. +inline "cic:/CoRN/ftc/Rolle/Hab'.var". -inline cic:/CoRN/ftc/Rolle/Hab.con. +inline "cic:/CoRN/ftc/Rolle/Hab.con". -inline cic:/CoRN/ftc/Rolle/I.con. +inline "cic:/CoRN/ftc/Rolle/I.con". -inline cic:/CoRN/ftc/Rolle/F.var. +inline "cic:/CoRN/ftc/Rolle/F.var". -inline cic:/CoRN/ftc/Rolle/F'.var. +inline "cic:/CoRN/ftc/Rolle/F'.var". -inline cic:/CoRN/ftc/Rolle/derF.var. +inline "cic:/CoRN/ftc/Rolle/derF.var". -inline cic:/CoRN/ftc/Rolle/Ha.var. +inline "cic:/CoRN/ftc/Rolle/Ha.var". -inline cic:/CoRN/ftc/Rolle/Hb.var. +inline "cic:/CoRN/ftc/Rolle/Hb.var". (* end hide *) (* begin show *) -inline cic:/CoRN/ftc/Rolle/Fab.var. +inline "cic:/CoRN/ftc/Rolle/Fab.var". (* end show *) (* begin hide *) -inline cic:/CoRN/ftc/Rolle/e.var. +inline "cic:/CoRN/ftc/Rolle/e.var". -inline cic:/CoRN/ftc/Rolle/He.var. +inline "cic:/CoRN/ftc/Rolle/He.var". -inline cic:/CoRN/ftc/Rolle/contF'.con. +inline "cic:/CoRN/ftc/Rolle/contF'.con". -inline cic:/CoRN/ftc/Rolle/derivF.con. +inline "cic:/CoRN/ftc/Rolle/derivF.con". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma2.con. +inline "cic:/CoRN/ftc/Rolle/Rolle_lemma2.con". -inline cic:/CoRN/ftc/Rolle/df.con. +inline "cic:/CoRN/ftc/Rolle/df.con". -inline cic:/CoRN/ftc/Rolle/Hdf.con. +inline "cic:/CoRN/ftc/Rolle/Hdf.con". -inline cic:/CoRN/ftc/Rolle/Hf.con. +inline "cic:/CoRN/ftc/Rolle/Hf.con". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma3.con. +inline "cic:/CoRN/ftc/Rolle/Rolle_lemma3.con". -inline cic:/CoRN/ftc/Rolle/df'.con. +inline "cic:/CoRN/ftc/Rolle/df'.con". -inline cic:/CoRN/ftc/Rolle/Hdf'.con. +inline "cic:/CoRN/ftc/Rolle/Hdf'.con". -inline cic:/CoRN/ftc/Rolle/Hf'.con. +inline "cic:/CoRN/ftc/Rolle/Hf'.con". -inline cic:/CoRN/ftc/Rolle/d.con. +inline "cic:/CoRN/ftc/Rolle/d.con". -inline cic:/CoRN/ftc/Rolle/Hd.con. +inline "cic:/CoRN/ftc/Rolle/Hd.con". -inline cic:/CoRN/ftc/Rolle/incF.con. +inline "cic:/CoRN/ftc/Rolle/incF.con". -inline cic:/CoRN/ftc/Rolle/n.con. +inline "cic:/CoRN/ftc/Rolle/n.con". -inline cic:/CoRN/ftc/Rolle/fcp.con. +inline "cic:/CoRN/ftc/Rolle/fcp.con". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma1.con. +inline "cic:/CoRN/ftc/Rolle/Rolle_lemma1.con". -inline cic:/CoRN/ftc/Rolle/incF'.con. +inline "cic:/CoRN/ftc/Rolle/incF'.con". -inline cic:/CoRN/ftc/Rolle/fcp'.con. +inline "cic:/CoRN/ftc/Rolle/fcp'.con". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma4.con. +inline "cic:/CoRN/ftc/Rolle/Rolle_lemma4.con". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma5.con. +inline "cic:/CoRN/ftc/Rolle/Rolle_lemma5.con". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma6.con. +inline "cic:/CoRN/ftc/Rolle/Rolle_lemma6.con". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma7.con. +inline "cic:/CoRN/ftc/Rolle/Rolle_lemma7.con". -inline cic:/CoRN/ftc/Rolle/j.con. +inline "cic:/CoRN/ftc/Rolle/j.con". -inline cic:/CoRN/ftc/Rolle/Hj.con. +inline "cic:/CoRN/ftc/Rolle/Hj.con". -inline cic:/CoRN/ftc/Rolle/Hj'.con. +inline "cic:/CoRN/ftc/Rolle/Hj'.con". -inline cic:/CoRN/ftc/Rolle/k.con. +inline "cic:/CoRN/ftc/Rolle/k.con". -inline cic:/CoRN/ftc/Rolle/Hk.con. +inline "cic:/CoRN/ftc/Rolle/Hk.con". -inline cic:/CoRN/ftc/Rolle/Hk'.con. +inline "cic:/CoRN/ftc/Rolle/Hk'.con". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma8.con. +inline "cic:/CoRN/ftc/Rolle/Rolle_lemma8.con". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma9.con. +inline "cic:/CoRN/ftc/Rolle/Rolle_lemma9.con". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma10.con. +inline "cic:/CoRN/ftc/Rolle/Rolle_lemma10.con". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma11.con. +inline "cic:/CoRN/ftc/Rolle/Rolle_lemma11.con". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma12.con. +inline "cic:/CoRN/ftc/Rolle/Rolle_lemma12.con". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma13.con. +inline "cic:/CoRN/ftc/Rolle/Rolle_lemma13.con". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma15.con. +inline "cic:/CoRN/ftc/Rolle/Rolle_lemma15.con". (* end hide *) -inline cic:/CoRN/ftc/Rolle/Rolle.con. +inline "cic:/CoRN/ftc/Rolle/Rolle.con". (* UNEXPORTED End Rolle. @@ -164,35 +162,35 @@ Section Law_of_the_Mean. The following is a simple corollary: *) -inline cic:/CoRN/ftc/Rolle/a.var. +inline "cic:/CoRN/ftc/Rolle/a.var". -inline cic:/CoRN/ftc/Rolle/b.var. +inline "cic:/CoRN/ftc/Rolle/b.var". -inline cic:/CoRN/ftc/Rolle/Hab'.var. +inline "cic:/CoRN/ftc/Rolle/Hab'.var". (* begin hide *) -inline cic:/CoRN/ftc/Rolle/Hab.con. +inline "cic:/CoRN/ftc/Rolle/Hab.con". -inline cic:/CoRN/ftc/Rolle/I.con. +inline "cic:/CoRN/ftc/Rolle/I.con". (* end hide *) -inline cic:/CoRN/ftc/Rolle/F.var. +inline "cic:/CoRN/ftc/Rolle/F.var". -inline cic:/CoRN/ftc/Rolle/F'.var. +inline "cic:/CoRN/ftc/Rolle/F'.var". -inline cic:/CoRN/ftc/Rolle/HF.var. +inline "cic:/CoRN/ftc/Rolle/HF.var". (* begin show *) -inline cic:/CoRN/ftc/Rolle/HA.var. +inline "cic:/CoRN/ftc/Rolle/HA.var". -inline cic:/CoRN/ftc/Rolle/HB.var. +inline "cic:/CoRN/ftc/Rolle/HB.var". (* end show *) -inline cic:/CoRN/ftc/Rolle/Law_of_the_Mean_I.con. +inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean_I.con". (* UNEXPORTED End Law_of_the_Mean. @@ -206,29 +204,29 @@ Section Corollaries. We can also state these theorems without expliciting the derivative of [F]. *) -inline cic:/CoRN/ftc/Rolle/a.var. +inline "cic:/CoRN/ftc/Rolle/a.var". -inline cic:/CoRN/ftc/Rolle/b.var. +inline "cic:/CoRN/ftc/Rolle/b.var". -inline cic:/CoRN/ftc/Rolle/Hab'.var. +inline "cic:/CoRN/ftc/Rolle/Hab'.var". (* begin hide *) -inline cic:/CoRN/ftc/Rolle/Hab.con. +inline "cic:/CoRN/ftc/Rolle/Hab.con". (* end hide *) -inline cic:/CoRN/ftc/Rolle/F.var. +inline "cic:/CoRN/ftc/Rolle/F.var". (* begin show *) -inline cic:/CoRN/ftc/Rolle/HF.var. +inline "cic:/CoRN/ftc/Rolle/HF.var". (* end show *) -inline cic:/CoRN/ftc/Rolle/Rolle'.con. +inline "cic:/CoRN/ftc/Rolle/Rolle'.con". -inline cic:/CoRN/ftc/Rolle/Law_of_the_Mean'_I.con. +inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean'_I.con". (* UNEXPORTED End Corollaries. @@ -248,35 +246,35 @@ state it also in this form. %\end{convention}% *) -inline cic:/CoRN/ftc/Rolle/I.var. +inline "cic:/CoRN/ftc/Rolle/I.var". -inline cic:/CoRN/ftc/Rolle/pI.var. +inline "cic:/CoRN/ftc/Rolle/pI.var". -inline cic:/CoRN/ftc/Rolle/F.var. +inline "cic:/CoRN/ftc/Rolle/F.var". -inline cic:/CoRN/ftc/Rolle/F'.var. +inline "cic:/CoRN/ftc/Rolle/F'.var". (* begin show *) -inline cic:/CoRN/ftc/Rolle/derF.var. +inline "cic:/CoRN/ftc/Rolle/derF.var". (* end show *) (* begin hide *) -inline cic:/CoRN/ftc/Rolle/incF.con. +inline "cic:/CoRN/ftc/Rolle/incF.con". -inline cic:/CoRN/ftc/Rolle/incF'.con. +inline "cic:/CoRN/ftc/Rolle/incF'.con". (* end hide *) -inline cic:/CoRN/ftc/Rolle/Law_of_the_Mean.con. +inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean.con". (*#* We further generalize the mean law by writing as an explicit bound. *) -inline cic:/CoRN/ftc/Rolle/Law_of_the_Mean_ineq.con. +inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean_ineq.con". (* UNEXPORTED End Generalizations.