X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FStrongIVT.ma;h=fd99ff05a3e293c0b9f998c30b3a4ab165e51ece;hb=54d09097e4ddbf7383d47ff0df4f1d9e14ea50fc;hp=b27af136a31ade7a3e88d1a16b79f228b4dc3706;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/StrongIVT.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/StrongIVT.ma index b27af136a..fd99ff05a 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/StrongIVT.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/StrongIVT.ma @@ -16,18 +16,16 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/StrongIVT". +include "CoRN.ma". + (* $Id: StrongIVT.v,v 1.5 2004/04/23 10:01:01 lcf Exp $ *) -(* INCLUDE -WeakIVT -*) +include "ftc/WeakIVT.ma". -(* INCLUDE -CalculusTheorems -*) +include "ftc/CalculusTheorems.ma". (* UNEXPORTED -Section IVT'. +Section IVT' *) (*#* ** Strong IVT for partial functions @@ -38,106 +36,106 @@ part, we will simply do that, repeating the previous construction. The same notations and conventions apply as before. *) -inline cic:/CoRN/ftc/StrongIVT/a.var. +alias id "a" = "cic:/CoRN/ftc/StrongIVT/IVT'/a.var". -inline cic:/CoRN/ftc/StrongIVT/b.var. +alias id "b" = "cic:/CoRN/ftc/StrongIVT/IVT'/b.var". -inline cic:/CoRN/ftc/StrongIVT/Hab'.var. +alias id "Hab'" = "cic:/CoRN/ftc/StrongIVT/IVT'/Hab'.var". -inline cic:/CoRN/ftc/StrongIVT/Hab.var. +alias id "Hab" = "cic:/CoRN/ftc/StrongIVT/IVT'/Hab.var". (* begin hide *) -inline cic:/CoRN/ftc/StrongIVT/I.con. +inline "cic:/CoRN/ftc/StrongIVT/IVT'/I.con" "IVT'__". -inline cic:/CoRN/ftc/StrongIVT/I'.con. +inline "cic:/CoRN/ftc/StrongIVT/IVT'/I'.con" "IVT'__". (* end hide *) -inline cic:/CoRN/ftc/StrongIVT/F.var. +alias id "F" = "cic:/CoRN/ftc/StrongIVT/IVT'/F.var". -inline cic:/CoRN/ftc/StrongIVT/contF.var. +alias id "contF" = "cic:/CoRN/ftc/StrongIVT/IVT'/contF.var". (* begin hide *) -inline cic:/CoRN/ftc/StrongIVT/incF.con. +inline "cic:/CoRN/ftc/StrongIVT/IVT'/incF.con" "IVT'__". (* end hide *) (* begin show *) -inline cic:/CoRN/ftc/StrongIVT/incrF.var. +alias id "incrF" = "cic:/CoRN/ftc/StrongIVT/IVT'/incrF.var". (* end show *) (* begin hide *) -inline cic:/CoRN/ftc/StrongIVT/Ha.con. +inline "cic:/CoRN/ftc/StrongIVT/IVT'/Ha.con" "IVT'__". -inline cic:/CoRN/ftc/StrongIVT/Hb.con. +inline "cic:/CoRN/ftc/StrongIVT/IVT'/Hb.con" "IVT'__". -inline cic:/CoRN/ftc/StrongIVT/HFab'.con. +inline "cic:/CoRN/ftc/StrongIVT/IVT'/HFab'.con" "IVT'__". (* end hide *) (* begin show *) -inline cic:/CoRN/ftc/StrongIVT/z.var. +alias id "z" = "cic:/CoRN/ftc/StrongIVT/IVT'/z.var". -inline cic:/CoRN/ftc/StrongIVT/Haz.var. +alias id "Haz" = "cic:/CoRN/ftc/StrongIVT/IVT'/Haz.var". -inline cic:/CoRN/ftc/StrongIVT/Hzb.var. +alias id "Hzb" = "cic:/CoRN/ftc/StrongIVT/IVT'/Hzb.var". (* end show *) -inline cic:/CoRN/ftc/StrongIVT/IVT'_seq_lemma.con. +inline "cic:/CoRN/ftc/StrongIVT/IVT'_seq_lemma.con". (* end hide *) -inline cic:/CoRN/ftc/StrongIVT/IVT'_aux_seq_type.ind. +inline "cic:/CoRN/ftc/StrongIVT/IVT'_aux_seq_type.ind". -inline cic:/CoRN/ftc/StrongIVT/IVT'_iter.con. +inline "cic:/CoRN/ftc/StrongIVT/IVT'_iter.con". -inline cic:/CoRN/ftc/StrongIVT/IVT'_seq.con. +inline "cic:/CoRN/ftc/StrongIVT/IVT'_seq.con". -inline cic:/CoRN/ftc/StrongIVT/a'_seq.con. +inline "cic:/CoRN/ftc/StrongIVT/a'_seq.con". -inline cic:/CoRN/ftc/StrongIVT/b'_seq.con. +inline "cic:/CoRN/ftc/StrongIVT/b'_seq.con". -inline cic:/CoRN/ftc/StrongIVT/a'_seq_I.con. +inline "cic:/CoRN/ftc/StrongIVT/a'_seq_I.con". -inline cic:/CoRN/ftc/StrongIVT/b'_seq_I.con. +inline "cic:/CoRN/ftc/StrongIVT/b'_seq_I.con". -inline cic:/CoRN/ftc/StrongIVT/a'_seq_less_b'_seq.con. +inline "cic:/CoRN/ftc/StrongIVT/a'_seq_less_b'_seq.con". -inline cic:/CoRN/ftc/StrongIVT/a'_seq_less_z.con. +inline "cic:/CoRN/ftc/StrongIVT/a'_seq_less_z.con". -inline cic:/CoRN/ftc/StrongIVT/z_less_b'_seq.con. +inline "cic:/CoRN/ftc/StrongIVT/z_less_b'_seq.con". -inline cic:/CoRN/ftc/StrongIVT/a'_seq_mon.con. +inline "cic:/CoRN/ftc/StrongIVT/a'_seq_mon.con". -inline cic:/CoRN/ftc/StrongIVT/b'_seq_mon.con. +inline "cic:/CoRN/ftc/StrongIVT/b'_seq_mon.con". -inline cic:/CoRN/ftc/StrongIVT/a'_seq_b'_seq_dist_n.con. +inline "cic:/CoRN/ftc/StrongIVT/a'_seq_b'_seq_dist_n.con". -inline cic:/CoRN/ftc/StrongIVT/a'_seq_b'_seq_dist.con. +inline "cic:/CoRN/ftc/StrongIVT/a'_seq_b'_seq_dist.con". -inline cic:/CoRN/ftc/StrongIVT/a'_seq_Cauchy.con. +inline "cic:/CoRN/ftc/StrongIVT/a'_seq_Cauchy.con". -inline cic:/CoRN/ftc/StrongIVT/b'_seq_Cauchy.con. +inline "cic:/CoRN/ftc/StrongIVT/b'_seq_Cauchy.con". -inline cic:/CoRN/ftc/StrongIVT/xa.con. +inline "cic:/CoRN/ftc/StrongIVT/IVT'/xa.con" "IVT'__". -inline cic:/CoRN/ftc/StrongIVT/xb.con. +inline "cic:/CoRN/ftc/StrongIVT/IVT'/xb.con" "IVT'__". -inline cic:/CoRN/ftc/StrongIVT/a'_seq_b'_seq_lim.con. +inline "cic:/CoRN/ftc/StrongIVT/a'_seq_b'_seq_lim.con". -inline cic:/CoRN/ftc/StrongIVT/xa'_in_interval.con. +inline "cic:/CoRN/ftc/StrongIVT/xa'_in_interval.con". -inline cic:/CoRN/ftc/StrongIVT/IVT'_I.con. +inline "cic:/CoRN/ftc/StrongIVT/IVT'_I.con". (* UNEXPORTED -End IVT'. +End IVT' *) (*#* **Other formulations @@ -146,21 +144,21 @@ We now generalize the various statements of the intermediate value theorem to more widely applicable forms. *) -inline cic:/CoRN/ftc/StrongIVT/Weak_IVT.con. +inline "cic:/CoRN/ftc/StrongIVT/Weak_IVT.con". -inline cic:/CoRN/ftc/StrongIVT/IVT_inc.con. +inline "cic:/CoRN/ftc/StrongIVT/IVT_inc.con". (* UNEXPORTED Transparent Min. *) -inline cic:/CoRN/ftc/StrongIVT/IVT_dec.con. +inline "cic:/CoRN/ftc/StrongIVT/IVT_dec.con". -inline cic:/CoRN/ftc/StrongIVT/IVT'_inc.con. +inline "cic:/CoRN/ftc/StrongIVT/IVT'_inc.con". (* UNEXPORTED Transparent Min. *) -inline cic:/CoRN/ftc/StrongIVT/IVT'_dec.con. +inline "cic:/CoRN/ftc/StrongIVT/IVT'_dec.con".