X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FMoreIntegrals.ma;h=f48c65d405744424c9245d69640e5e2c637b29e7;hb=bb691187f8bbe22ec37ca41f9f3f42f9d8e505df;hp=062018bf97caea93fe06710fd26f4854b9b4affb;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntegrals.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntegrals.ma index 062018bf9..f48c65d40 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntegrals.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntegrals.ma @@ -16,15 +16,13 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/MoreIntegrals". +include "CoRN_notation.ma". + (* $Id: MoreIntegrals.v,v 1.6 2004/04/23 10:00:59 lcf Exp $ *) -(* INCLUDE -Integral -*) +include "ftc/Integral.ma". -(* INCLUDE -MoreFunctions -*) +include "ftc/MoreFunctions.ma". (* UNEXPORTED Section Lemmas. @@ -50,15 +48,15 @@ partial functions continuous in [[Min(a,b),Max(a,b)]]. Before we define the new integral we need to some trivial interval inclusions. *) -inline cic:/CoRN/ftc/MoreIntegrals/a.var. +inline "cic:/CoRN/ftc/MoreIntegrals/a.var". -inline cic:/CoRN/ftc/MoreIntegrals/b.var. +inline "cic:/CoRN/ftc/MoreIntegrals/b.var". -inline cic:/CoRN/ftc/MoreIntegrals/Hab.var. +inline "cic:/CoRN/ftc/MoreIntegrals/Hab.var". -inline cic:/CoRN/ftc/MoreIntegrals/compact_inc_Min_lft.con. +inline "cic:/CoRN/ftc/MoreIntegrals/compact_inc_Min_lft.con". -inline cic:/CoRN/ftc/MoreIntegrals/compact_inc_Min_rht.con. +inline "cic:/CoRN/ftc/MoreIntegrals/compact_inc_Min_rht.con". (* UNEXPORTED End Lemmas. @@ -76,23 +74,23 @@ classical definition, and it collapses to the old one in the case [a [<=] b]. *) -inline cic:/CoRN/ftc/MoreIntegrals/a.var. +inline "cic:/CoRN/ftc/MoreIntegrals/a.var". -inline cic:/CoRN/ftc/MoreIntegrals/b.var. +inline "cic:/CoRN/ftc/MoreIntegrals/b.var". -inline cic:/CoRN/ftc/MoreIntegrals/Hab.var. +inline "cic:/CoRN/ftc/MoreIntegrals/Hab.var". -inline cic:/CoRN/ftc/MoreIntegrals/F.var. +inline "cic:/CoRN/ftc/MoreIntegrals/F.var". -inline cic:/CoRN/ftc/MoreIntegrals/HF.var. +inline "cic:/CoRN/ftc/MoreIntegrals/HF.var". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_inc1.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_inc1.con". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_inc2.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_inc2.con". -inline cic:/CoRN/ftc/MoreIntegrals/Integral.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral.con". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_integral.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_integral.con". (* UNEXPORTED End Definitions. @@ -112,55 +110,55 @@ All our old properties carry over to this new definition---and some new ones, too. We begin with (strong) extensionality. *) -inline cic:/CoRN/ftc/MoreIntegrals/a.var. +inline "cic:/CoRN/ftc/MoreIntegrals/a.var". -inline cic:/CoRN/ftc/MoreIntegrals/b.var. +inline "cic:/CoRN/ftc/MoreIntegrals/b.var". -inline cic:/CoRN/ftc/MoreIntegrals/Hab.var. +inline "cic:/CoRN/ftc/MoreIntegrals/Hab.var". -inline cic:/CoRN/ftc/MoreIntegrals/F.var. +inline "cic:/CoRN/ftc/MoreIntegrals/F.var". -inline cic:/CoRN/ftc/MoreIntegrals/G.var. +inline "cic:/CoRN/ftc/MoreIntegrals/G.var". -inline cic:/CoRN/ftc/MoreIntegrals/contF.var. +inline "cic:/CoRN/ftc/MoreIntegrals/contF.var". -inline cic:/CoRN/ftc/MoreIntegrals/contG.var. +inline "cic:/CoRN/ftc/MoreIntegrals/contG.var". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_strext.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_strext.con". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_strext'.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_strext'.con". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_wd.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_wd.con". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_wd'.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_wd'.con". (*#* The integral is a linear operator. *) -inline cic:/CoRN/ftc/MoreIntegrals/Integral_const.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_const.con". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_comm_scal.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_comm_scal.con". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_plus.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_plus.con". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_inv.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_inv.con". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_minus.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_minus.con". -inline cic:/CoRN/ftc/MoreIntegrals/linear_Integral.con. +inline "cic:/CoRN/ftc/MoreIntegrals/linear_Integral.con". (*#* If the endpoints are equal then the integral vanishes. *) -inline cic:/CoRN/ftc/MoreIntegrals/Integral_empty.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_empty.con". (*#* And the norm provides an upper bound for the absolute value of the integral. *) -inline cic:/CoRN/ftc/MoreIntegrals/Integral_leEq_norm.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_leEq_norm.con". (* UNEXPORTED End Properties_of_Integral. @@ -174,9 +172,9 @@ Section More_Properties. Two other ways of stating the addition law for domains. *) -inline cic:/CoRN/ftc/MoreIntegrals/integral_plus_Integral.con. +inline "cic:/CoRN/ftc/MoreIntegrals/integral_plus_Integral.con". -inline cic:/CoRN/ftc/MoreIntegrals/integral_plus_integral'.con. +inline "cic:/CoRN/ftc/MoreIntegrals/integral_plus_integral'.con". (*#* And now we can prove the addition law for domains with our general operator. @@ -185,81 +183,81 @@ And now we can prove the addition law for domains with our general operator. %\end{convention}% *) -inline cic:/CoRN/ftc/MoreIntegrals/a.var. +inline "cic:/CoRN/ftc/MoreIntegrals/a.var". -inline cic:/CoRN/ftc/MoreIntegrals/b.var. +inline "cic:/CoRN/ftc/MoreIntegrals/b.var". -inline cic:/CoRN/ftc/MoreIntegrals/c.var. +inline "cic:/CoRN/ftc/MoreIntegrals/c.var". (* begin show *) -inline cic:/CoRN/ftc/MoreIntegrals/Hab'.var. +inline "cic:/CoRN/ftc/MoreIntegrals/Hab'.var". -inline cic:/CoRN/ftc/MoreIntegrals/Hac'.var. +inline "cic:/CoRN/ftc/MoreIntegrals/Hac'.var". -inline cic:/CoRN/ftc/MoreIntegrals/Hcb'.var. +inline "cic:/CoRN/ftc/MoreIntegrals/Hcb'.var". -inline cic:/CoRN/ftc/MoreIntegrals/Habc'.var. +inline "cic:/CoRN/ftc/MoreIntegrals/Habc'.var". (* end show *) -inline cic:/CoRN/ftc/MoreIntegrals/F.var. +inline "cic:/CoRN/ftc/MoreIntegrals/F.var". (* begin show *) -inline cic:/CoRN/ftc/MoreIntegrals/Hab.var. +inline "cic:/CoRN/ftc/MoreIntegrals/Hab.var". -inline cic:/CoRN/ftc/MoreIntegrals/Hac.var. +inline "cic:/CoRN/ftc/MoreIntegrals/Hac.var". -inline cic:/CoRN/ftc/MoreIntegrals/Hcb.var. +inline "cic:/CoRN/ftc/MoreIntegrals/Hcb.var". -inline cic:/CoRN/ftc/MoreIntegrals/Habc.var. +inline "cic:/CoRN/ftc/MoreIntegrals/Habc.var". (* end show *) (* begin hide *) -inline cic:/CoRN/ftc/MoreIntegrals/le_abc_ab.con. +inline "cic:/CoRN/ftc/MoreIntegrals/le_abc_ab.con". -inline cic:/CoRN/ftc/MoreIntegrals/le_abc_ac.con. +inline "cic:/CoRN/ftc/MoreIntegrals/le_abc_ac.con". -inline cic:/CoRN/ftc/MoreIntegrals/le_abc_cb.con. +inline "cic:/CoRN/ftc/MoreIntegrals/le_abc_cb.con". -inline cic:/CoRN/ftc/MoreIntegrals/le_abc_a.con. +inline "cic:/CoRN/ftc/MoreIntegrals/le_abc_a.con". -inline cic:/CoRN/ftc/MoreIntegrals/le_abc_b.con. +inline "cic:/CoRN/ftc/MoreIntegrals/le_abc_b.con". -inline cic:/CoRN/ftc/MoreIntegrals/le_abc_c.con. +inline "cic:/CoRN/ftc/MoreIntegrals/le_abc_c.con". -inline cic:/CoRN/ftc/MoreIntegrals/le_ab_a.con. +inline "cic:/CoRN/ftc/MoreIntegrals/le_ab_a.con". -inline cic:/CoRN/ftc/MoreIntegrals/le_cb_c.con. +inline "cic:/CoRN/ftc/MoreIntegrals/le_cb_c.con". -inline cic:/CoRN/ftc/MoreIntegrals/le_ac_a.con. +inline "cic:/CoRN/ftc/MoreIntegrals/le_ac_a.con". -inline cic:/CoRN/ftc/MoreIntegrals/le_ab_b.con. +inline "cic:/CoRN/ftc/MoreIntegrals/le_ab_b.con". -inline cic:/CoRN/ftc/MoreIntegrals/le_cb_b.con. +inline "cic:/CoRN/ftc/MoreIntegrals/le_cb_b.con". -inline cic:/CoRN/ftc/MoreIntegrals/le_ac_c.con. +inline "cic:/CoRN/ftc/MoreIntegrals/le_ac_c.con". -inline cic:/CoRN/ftc/MoreIntegrals/Habc_abc.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Habc_abc.con". -inline cic:/CoRN/ftc/MoreIntegrals/Habc_ab.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Habc_ab.con". -inline cic:/CoRN/ftc/MoreIntegrals/Habc_ac.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Habc_ac.con". -inline cic:/CoRN/ftc/MoreIntegrals/Habc_cb.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Habc_cb.con". -inline cic:/CoRN/ftc/MoreIntegrals/Habc_a.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Habc_a.con". -inline cic:/CoRN/ftc/MoreIntegrals/Habc_b.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Habc_b.con". -inline cic:/CoRN/ftc/MoreIntegrals/Habc_c.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Habc_c.con". (* end hide *) -inline cic:/CoRN/ftc/MoreIntegrals/Integral_plus_Integral.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_plus_Integral.con". (*#* Notice that, unlike in the classical case, an extra hypothesis (the @@ -274,31 +272,31 @@ End More_Properties. Section Corollaries. *) -inline cic:/CoRN/ftc/MoreIntegrals/a.var. +inline "cic:/CoRN/ftc/MoreIntegrals/a.var". -inline cic:/CoRN/ftc/MoreIntegrals/b.var. +inline "cic:/CoRN/ftc/MoreIntegrals/b.var". -inline cic:/CoRN/ftc/MoreIntegrals/Hab.var. +inline "cic:/CoRN/ftc/MoreIntegrals/Hab.var". -inline cic:/CoRN/ftc/MoreIntegrals/F.var. +inline "cic:/CoRN/ftc/MoreIntegrals/F.var". -inline cic:/CoRN/ftc/MoreIntegrals/contF.var. +inline "cic:/CoRN/ftc/MoreIntegrals/contF.var". (*#* As a corollary, we get the following rule: *) -inline cic:/CoRN/ftc/MoreIntegrals/Integral_op.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_op.con". (*#* Finally, some miscellaneous results: *) -inline cic:/CoRN/ftc/MoreIntegrals/Integral_less_norm.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_less_norm.con". -inline cic:/CoRN/ftc/MoreIntegrals/ub_Integral.con. +inline "cic:/CoRN/ftc/MoreIntegrals/ub_Integral.con". (* UNEXPORTED End Corollaries. *) -inline cic:/CoRN/ftc/MoreIntegrals/Integral_ap_zero.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_ap_zero.con". -inline cic:/CoRN/ftc/MoreIntegrals/Integral_eq_zero.con. +inline "cic:/CoRN/ftc/MoreIntegrals/Integral_eq_zero.con".