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=842e243be954d67360788d08701289f3237c2699;hp=7eda2c5ae097b6ce4dd683ee12bf2b1733d6833f;hpb=876f16ec4e9080bad4e39bd9c203d6529dcf4f56;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 7eda2c5ae..01273b08a 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/Rolle.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/Rolle.ma @@ -25,7 +25,7 @@ include "tactics/DiffTactics2.ma". include "ftc/MoreFunctions.ma". (* UNEXPORTED -Section Rolle. +Section Rolle *) (*#* *Rolle's Theorem @@ -42,189 +42,189 @@ 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". (* 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". (* 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 *) @@ -233,11 +233,11 @@ inline "cic:/CoRN/ftc/Rolle/Rolle'.con". inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean'_I.con". (* UNEXPORTED -End Corollaries. +End Corollaries *) (* UNEXPORTED -Section Generalizations. +Section Generalizations *) (*#* @@ -250,25 +250,25 @@ 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 *) @@ -281,6 +281,6 @@ We further generalize the mean law by writing as an explicit bound. inline "cic:/CoRN/ftc/Rolle/Law_of_the_Mean_ineq.con". (* UNEXPORTED -End Generalizations. +End Generalizations *)