X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FIntegral.ma;h=4a8a416889f63ff203a435def98df31b96ea3eaa;hb=1d8389a897e804825909cc84640e0d5c5f58e543;hp=a6bace36da9fccd03eac78c70e164e743c9bbc5b;hpb=876f16ec4e9080bad4e39bd9c203d6529dcf4f56;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/Integral.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/Integral.ma index a6bace36d..4a8a41688 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/Integral.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/Integral.ma @@ -29,21 +29,21 @@ include "ftc/RefLemma.ma". (* begin hide *) (* UNEXPORTED -Section Lemmas. +Section Lemmas *) -inline "cic:/CoRN/ftc/Integral/Sumx_wd_weird.con". +inline "cic:/CoRN/ftc/Integral/Lemmas/Sumx_wd_weird.con" "Lemmas__". inline "cic:/CoRN/ftc/Integral/Sumx_weird_lemma.con". (* UNEXPORTED -End Lemmas. +End Lemmas *) (* end hide *) (* UNEXPORTED -Section Integral. +Section Integral *) (*#* *Integral @@ -59,26 +59,26 @@ continuous functions in [I]. %\end{convention}% *) -inline "cic:/CoRN/ftc/Integral/a.var". +alias id "a" = "cic:/CoRN/ftc/Integral/Integral/a.var". -inline "cic:/CoRN/ftc/Integral/b.var". +alias id "b" = "cic:/CoRN/ftc/Integral/Integral/b.var". -inline "cic:/CoRN/ftc/Integral/Hab.var". +alias id "Hab" = "cic:/CoRN/ftc/Integral/Integral/Hab.var". (* begin hide *) -inline "cic:/CoRN/ftc/Integral/I.con". +inline "cic:/CoRN/ftc/Integral/Integral/I.con" "Integral__". -inline "cic:/CoRN/ftc/Integral/F.var". +alias id "F" = "cic:/CoRN/ftc/Integral/Integral/F.var". -inline "cic:/CoRN/ftc/Integral/contF.var". +alias id "contF" = "cic:/CoRN/ftc/Integral/Integral/contF.var". -inline "cic:/CoRN/ftc/Integral/contF'.con". +inline "cic:/CoRN/ftc/Integral/Integral/contF'.con" "Integral__". (* end hide *) (* UNEXPORTED -Section Darboux_Sum. +Section Darboux_Sum *) inline "cic:/CoRN/ftc/Integral/integral_seq.con". @@ -88,11 +88,11 @@ inline "cic:/CoRN/ftc/Integral/Cauchy_Darboux_Seq.con". inline "cic:/CoRN/ftc/Integral/integral.con". (* UNEXPORTED -End Darboux_Sum. +End Darboux_Sum *) (* UNEXPORTED -Section Integral_Thm. +Section Integral_Thm *) (*#* @@ -106,57 +106,57 @@ respecting [P]. %\end{convention}% *) -inline "cic:/CoRN/ftc/Integral/n.var". +alias id "n" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/n.var". -inline "cic:/CoRN/ftc/Integral/P.var". +alias id "P" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/P.var". -inline "cic:/CoRN/ftc/Integral/e.var". +alias id "e" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/e.var". -inline "cic:/CoRN/ftc/Integral/He.var". +alias id "He" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/He.var". (* begin hide *) -inline "cic:/CoRN/ftc/Integral/d.con". +inline "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/d.con" "Integral__Integral_Thm__". (* end hide *) -inline "cic:/CoRN/ftc/Integral/HmeshP.var". +alias id "HmeshP" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HmeshP.var". -inline "cic:/CoRN/ftc/Integral/fP.var". +alias id "fP" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/fP.var". -inline "cic:/CoRN/ftc/Integral/HfP.var". +alias id "HfP" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HfP.var". -inline "cic:/CoRN/ftc/Integral/HfP'.var". +alias id "HfP'" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/HfP'.var". -inline "cic:/CoRN/ftc/Integral/incF.var". +alias id "incF" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/incF.var". inline "cic:/CoRN/ftc/Integral/partition_Sum_conv_integral.con". (* UNEXPORTED -End Integral_Thm. +End Integral_Thm *) (* UNEXPORTED -End Integral. +End Integral *) (* UNEXPORTED -Section Basic_Properties. +Section Basic_Properties *) (*#* The usual extensionality and strong extensionality results hold. *) -inline "cic:/CoRN/ftc/Integral/a.var". +alias id "a" = "cic:/CoRN/ftc/Integral/Basic_Properties/a.var". -inline "cic:/CoRN/ftc/Integral/b.var". +alias id "b" = "cic:/CoRN/ftc/Integral/Basic_Properties/b.var". -inline "cic:/CoRN/ftc/Integral/Hab.var". +alias id "Hab" = "cic:/CoRN/ftc/Integral/Basic_Properties/Hab.var". (* begin hide *) -inline "cic:/CoRN/ftc/Integral/I.con". +inline "cic:/CoRN/ftc/Integral/Basic_Properties/I.con" "Basic_Properties__". (* end hide *) @@ -165,16 +165,16 @@ Notation Integral := (integral _ _ Hab). *) (* UNEXPORTED -Section Well_Definedness. +Section Well_Definedness *) -inline "cic:/CoRN/ftc/Integral/F.var". +alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/F.var". -inline "cic:/CoRN/ftc/Integral/G.var". +alias id "G" = "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/G.var". -inline "cic:/CoRN/ftc/Integral/contF.var". +alias id "contF" = "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/contF.var". -inline "cic:/CoRN/ftc/Integral/contG.var". +alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/contG.var". inline "cic:/CoRN/ftc/Integral/integral_strext.con". @@ -185,11 +185,11 @@ inline "cic:/CoRN/ftc/Integral/integral_wd.con". inline "cic:/CoRN/ftc/Integral/integral_wd'.con". (* UNEXPORTED -End Well_Definedness. +End Well_Definedness *) (* UNEXPORTED -Section Linearity_and_Monotonicity. +Section Linearity_and_Monotonicity *) (* UNEXPORTED @@ -202,13 +202,13 @@ The integral is a linear and monotonous function; in order to prove these facts inline "cic:/CoRN/ftc/Integral/integral_one.con". -inline "cic:/CoRN/ftc/Integral/F.var". +alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/F.var". -inline "cic:/CoRN/ftc/Integral/G.var". +alias id "G" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/G.var". -inline "cic:/CoRN/ftc/Integral/contF.var". +alias id "contF" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/contF.var". -inline "cic:/CoRN/ftc/Integral/contG.var". +alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/contG.var". inline "cic:/CoRN/ftc/Integral/integral_comm_scal.con". @@ -221,20 +221,20 @@ Transparent Even_Partition. inline "cic:/CoRN/ftc/Integral/integral_empty.con". (* UNEXPORTED -End Linearity_and_Monotonicity. +End Linearity_and_Monotonicity *) (* UNEXPORTED -Section Linearity_and_Monotonicity'. +Section Linearity_and_Monotonicity' *) -inline "cic:/CoRN/ftc/Integral/F.var". +alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/F.var". -inline "cic:/CoRN/ftc/Integral/G.var". +alias id "G" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/G.var". -inline "cic:/CoRN/ftc/Integral/contF.var". +alias id "contF" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contF.var". -inline "cic:/CoRN/ftc/Integral/contG.var". +alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contG.var". (*#* %\begin{convention}% Let [alpha, beta : IR] and assume that @@ -242,17 +242,17 @@ inline "cic:/CoRN/ftc/Integral/contG.var". %\end{convention}% *) -inline "cic:/CoRN/ftc/Integral/alpha.var". +alias id "alpha" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/alpha.var". -inline "cic:/CoRN/ftc/Integral/beta.var". +alias id "beta" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/beta.var". (* begin hide *) -inline "cic:/CoRN/ftc/Integral/h.con". +inline "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/h.con" "Basic_Properties__Linearity_and_Monotonicity'__". (* end hide *) -inline "cic:/CoRN/ftc/Integral/contH.var". +alias id "contH" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contH.var". inline "cic:/CoRN/ftc/Integral/linear_integral.con". @@ -267,20 +267,20 @@ Transparent nring. *) (* UNEXPORTED -End Linearity_and_Monotonicity'. +End Linearity_and_Monotonicity' *) (* UNEXPORTED -Section Corollaries. +Section Corollaries *) -inline "cic:/CoRN/ftc/Integral/F.var". +alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/F.var". -inline "cic:/CoRN/ftc/Integral/G.var". +alias id "G" = "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/G.var". -inline "cic:/CoRN/ftc/Integral/contF.var". +alias id "contF" = "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/contF.var". -inline "cic:/CoRN/ftc/Integral/contG.var". +alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Corollaries/contG.var". (*#* As corollaries we can calculate integrals of group operations applied to functions. @@ -303,11 +303,11 @@ inline "cic:/CoRN/ftc/Integral/ub_integral.con". inline "cic:/CoRN/ftc/Integral/integral_leEq_norm.con". (* UNEXPORTED -End Corollaries. +End Corollaries *) (* UNEXPORTED -Section Integral_Sum. +Section Integral_Sum *) (*#* @@ -319,22 +319,22 @@ $c\in[a,b]$#c∈[a,b]#. %\end{convention}% *) -inline "cic:/CoRN/ftc/Integral/F.var". +alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/F.var". -inline "cic:/CoRN/ftc/Integral/c.var". +alias id "c" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/c.var". -inline "cic:/CoRN/ftc/Integral/Hac.var". +alias id "Hac" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hac.var". -inline "cic:/CoRN/ftc/Integral/Hcb.var". +alias id "Hcb" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hcb.var". -inline "cic:/CoRN/ftc/Integral/Hab'.var". +alias id "Hab'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hab'.var". -inline "cic:/CoRN/ftc/Integral/Hac'.var". +alias id "Hac'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hac'.var". -inline "cic:/CoRN/ftc/Integral/Hcb'.var". +alias id "Hcb'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Hcb'.var". (* UNEXPORTED -Section Partition_Join. +Section Partition_Join *) (*#* @@ -349,13 +349,13 @@ inequality). %\end{convention}% *) -inline "cic:/CoRN/ftc/Integral/n.var". +alias id "n" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/n.var". -inline "cic:/CoRN/ftc/Integral/m.var". +alias id "m" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/m.var". -inline "cic:/CoRN/ftc/Integral/P.var". +alias id "P" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/P.var". -inline "cic:/CoRN/ftc/Integral/Q.var". +alias id "Q" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/Q.var". (* begin hide *) @@ -392,17 +392,17 @@ inline "cic:/CoRN/ftc/Integral/partition_join.con". %\end{convention}% *) -inline "cic:/CoRN/ftc/Integral/fP.var". +alias id "fP" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/fP.var". -inline "cic:/CoRN/ftc/Integral/HfP.var". +alias id "HfP" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfP.var". -inline "cic:/CoRN/ftc/Integral/HfP'.var". +alias id "HfP'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfP'.var". -inline "cic:/CoRN/ftc/Integral/fQ.var". +alias id "fQ" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/fQ.var". -inline "cic:/CoRN/ftc/Integral/HfQ.var". +alias id "HfQ" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfQ.var". -inline "cic:/CoRN/ftc/Integral/HfQ'.var". +alias id "HfQ'" = "cic:/CoRN/ftc/Integral/Basic_Properties/Integral_Sum/Partition_Join/HfQ'.var". (* begin hide *) @@ -455,7 +455,7 @@ inline "cic:/CoRN/ftc/Integral/partition_join_Sum_lemma.con". inline "cic:/CoRN/ftc/Integral/partition_join_mesh.con". (* UNEXPORTED -End Partition_Join. +End Partition_Join *) (*#* @@ -469,7 +469,7 @@ Opaque Even_Partition. inline "cic:/CoRN/ftc/Integral/integral_plus_integral.con". (* UNEXPORTED -End Integral_Sum. +End Integral_Sum *) (* UNEXPORTED @@ -477,7 +477,7 @@ Transparent Even_Partition. *) (* UNEXPORTED -End Basic_Properties. +End Basic_Properties *) (*#*