X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FRolle.ma;h=01273b08a701c4496e4804257e8e384e6e6e0685;hb=601baed778a190b580982b588ebe49ba3f762b30;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..01273b08a 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/Rolle.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/Rolle.ma @@ -16,18 +16,16 @@ 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. +Section Rolle *) (*#* *Rolle's Theorem @@ -44,198 +42,202 @@ We now begin to work with partial functions. We begin by stating and proving Ro (* begin hide *) -inline cic:/CoRN/ftc/Rolle/a.var. +alias id "a" = "cic:/CoRN/ftc/Rolle/Rolle/a.var". -inline cic:/CoRN/ftc/Rolle/b.var. +alias id "b" = "cic:/CoRN/ftc/Rolle/Rolle/b.var". -inline cic:/CoRN/ftc/Rolle/Hab'.var. +alias id "Hab'" = "cic:/CoRN/ftc/Rolle/Rolle/Hab'.var". -inline cic:/CoRN/ftc/Rolle/Hab.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Hab.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/I.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/I.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/F.var. +alias id "F" = "cic:/CoRN/ftc/Rolle/Rolle/F.var". -inline cic:/CoRN/ftc/Rolle/F'.var. +alias id "F'" = "cic:/CoRN/ftc/Rolle/Rolle/F'.var". -inline cic:/CoRN/ftc/Rolle/derF.var. +alias id "derF" = "cic:/CoRN/ftc/Rolle/Rolle/derF.var". -inline cic:/CoRN/ftc/Rolle/Ha.var. +alias id "Ha" = "cic:/CoRN/ftc/Rolle/Rolle/Ha.var". -inline cic:/CoRN/ftc/Rolle/Hb.var. +alias id "Hb" = "cic:/CoRN/ftc/Rolle/Rolle/Hb.var". (* end hide *) (* begin show *) -inline cic:/CoRN/ftc/Rolle/Fab.var. +alias id "Fab" = "cic:/CoRN/ftc/Rolle/Rolle/Fab.var". (* end show *) (* begin hide *) -inline cic:/CoRN/ftc/Rolle/e.var. +alias id "e" = "cic:/CoRN/ftc/Rolle/Rolle/e.var". -inline cic:/CoRN/ftc/Rolle/He.var. +alias id "He" = "cic:/CoRN/ftc/Rolle/Rolle/He.var". -inline cic:/CoRN/ftc/Rolle/contF'.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/contF'.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/derivF.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/derivF.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma2.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma2.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/df.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/df.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/Hdf.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Hdf.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/Hf.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Hf.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma3.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma3.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/df'.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/df'.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/Hdf'.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Hdf'.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/Hf'.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Hf'.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/d.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/d.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/Hd.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Hd.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/incF.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/incF.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/n.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/n.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/fcp.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/fcp.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma1.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma1.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/incF'.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/incF'.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/fcp'.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/fcp'.con" "Rolle__". + +(* NOTATION +Notation cp := (compact_part a b Hab' d Hd). +*) -inline cic:/CoRN/ftc/Rolle/Rolle_lemma4.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma4.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma5.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma5.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma6.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma6.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma7.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma7.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/j.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/j.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/Hj.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Hj.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/Hj'.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Hj'.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/k.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/k.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/Hk.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Hk.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/Hk'.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Hk'.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma8.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma8.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma9.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma9.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma10.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma10.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma11.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma11.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma12.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma12.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma13.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma13.con" "Rolle__". -inline cic:/CoRN/ftc/Rolle/Rolle_lemma15.con. +inline "cic:/CoRN/ftc/Rolle/Rolle/Rolle_lemma15.con" "Rolle__". (* end hide *) -inline cic:/CoRN/ftc/Rolle/Rolle.con. +inline "cic:/CoRN/ftc/Rolle/Rolle.con". (* UNEXPORTED -End Rolle. +End Rolle *) (* UNEXPORTED -Section Law_of_the_Mean. +Section Law_of_the_Mean *) (*#* The following is a simple corollary: *) -inline cic:/CoRN/ftc/Rolle/a.var. +alias id "a" = "cic:/CoRN/ftc/Rolle/Law_of_the_Mean/a.var". -inline cic:/CoRN/ftc/Rolle/b.var. +alias id "b" = "cic:/CoRN/ftc/Rolle/Law_of_the_Mean/b.var". -inline cic:/CoRN/ftc/Rolle/Hab'.var. +alias id "Hab'" = "cic:/CoRN/ftc/Rolle/Law_of_the_Mean/Hab'.var". (* begin hide *) -inline cic:/CoRN/ftc/Rolle/Hab.con. +inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean/Hab.con" "Law_of_the_Mean__". -inline cic:/CoRN/ftc/Rolle/I.con. +inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean/I.con" "Law_of_the_Mean__". (* end hide *) -inline cic:/CoRN/ftc/Rolle/F.var. +alias id "F" = "cic:/CoRN/ftc/Rolle/Law_of_the_Mean/F.var". -inline cic:/CoRN/ftc/Rolle/F'.var. +alias id "F'" = "cic:/CoRN/ftc/Rolle/Law_of_the_Mean/F'.var". -inline cic:/CoRN/ftc/Rolle/HF.var. +alias id "HF" = "cic:/CoRN/ftc/Rolle/Law_of_the_Mean/HF.var". (* begin show *) -inline cic:/CoRN/ftc/Rolle/HA.var. +alias id "HA" = "cic:/CoRN/ftc/Rolle/Law_of_the_Mean/HA.var". -inline cic:/CoRN/ftc/Rolle/HB.var. +alias id "HB" = "cic:/CoRN/ftc/Rolle/Law_of_the_Mean/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. +End Law_of_the_Mean *) (* UNEXPORTED -Section Corollaries. +Section Corollaries *) (*#* We can also state these theorems without expliciting the derivative of [F]. *) -inline cic:/CoRN/ftc/Rolle/a.var. +alias id "a" = "cic:/CoRN/ftc/Rolle/Corollaries/a.var". -inline cic:/CoRN/ftc/Rolle/b.var. +alias id "b" = "cic:/CoRN/ftc/Rolle/Corollaries/b.var". -inline cic:/CoRN/ftc/Rolle/Hab'.var. +alias id "Hab'" = "cic:/CoRN/ftc/Rolle/Corollaries/Hab'.var". (* begin hide *) -inline cic:/CoRN/ftc/Rolle/Hab.con. +inline "cic:/CoRN/ftc/Rolle/Corollaries/Hab.con" "Corollaries__". (* end hide *) -inline cic:/CoRN/ftc/Rolle/F.var. +alias id "F" = "cic:/CoRN/ftc/Rolle/Corollaries/F.var". (* begin show *) -inline cic:/CoRN/ftc/Rolle/HF.var. +alias id "HF" = "cic:/CoRN/ftc/Rolle/Corollaries/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. +End Corollaries *) (* UNEXPORTED -Section Generalizations. +Section Generalizations *) (*#* @@ -248,37 +250,37 @@ state it also in this form. %\end{convention}% *) -inline cic:/CoRN/ftc/Rolle/I.var. +alias id "I" = "cic:/CoRN/ftc/Rolle/Generalizations/I.var". -inline cic:/CoRN/ftc/Rolle/pI.var. +alias id "pI" = "cic:/CoRN/ftc/Rolle/Generalizations/pI.var". -inline cic:/CoRN/ftc/Rolle/F.var. +alias id "F" = "cic:/CoRN/ftc/Rolle/Generalizations/F.var". -inline cic:/CoRN/ftc/Rolle/F'.var. +alias id "F'" = "cic:/CoRN/ftc/Rolle/Generalizations/F'.var". (* begin show *) -inline cic:/CoRN/ftc/Rolle/derF.var. +alias id "derF" = "cic:/CoRN/ftc/Rolle/Generalizations/derF.var". (* end show *) (* begin hide *) -inline cic:/CoRN/ftc/Rolle/incF.con. +inline "cic:/CoRN/ftc/Rolle/Generalizations/incF.con" "Generalizations__". -inline cic:/CoRN/ftc/Rolle/incF'.con. +inline "cic:/CoRN/ftc/Rolle/Generalizations/incF'.con" "Generalizations__". (* 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. +End Generalizations *)