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=20377cd037f6cc5eb9c6a5664354a8a0189d3f4f;hp=9241494f98e81846a9ed683b761104c7370b444e;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;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 9241494f9..4a8a41688 100644
--- a/helm/software/matita/contribs/CoRN-Decl/ftc/Integral.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/ftc/Integral.ma
@@ -16,11 +16,11 @@
set "baseuri" "cic:/matita/CoRN-Decl/ftc/Integral".
+include "CoRN.ma".
+
(* $Id: Integral.v,v 1.10 2004/04/23 10:00:59 lcf Exp $ *)
-(* INCLUDE
-RefLemma
-*)
+include "ftc/RefLemma.ma".
(*#* printing integral %\ensuremath{\int_I}% #∫I# *)
@@ -29,21 +29,21 @@ RefLemma
(* 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.
+inline "cic:/CoRN/ftc/Integral/Sumx_weird_lemma.con".
(* UNEXPORTED
-End Lemmas.
+End Lemmas
*)
(* end hide *)
(* UNEXPORTED
-Section Integral.
+Section Integral
*)
(*#* *Integral
@@ -59,40 +59,40 @@ 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.
+inline "cic:/CoRN/ftc/Integral/integral_seq.con".
-inline cic:/CoRN/ftc/Integral/Cauchy_Darboux_Seq.con.
+inline "cic:/CoRN/ftc/Integral/Cauchy_Darboux_Seq.con".
-inline cic:/CoRN/ftc/Integral/integral.con.
+inline "cic:/CoRN/ftc/Integral/integral.con".
(* UNEXPORTED
-End Darboux_Sum.
+End Darboux_Sum
*)
(* UNEXPORTED
-Section Integral_Thm.
+Section Integral_Thm
*)
(*#*
@@ -106,86 +106,90 @@ 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.
+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 *)
+(* NOTATION
+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.
+inline "cic:/CoRN/ftc/Integral/integral_strext.con".
-inline cic:/CoRN/ftc/Integral/integral_strext'.con.
+inline "cic:/CoRN/ftc/Integral/integral_strext'.con".
-inline cic:/CoRN/ftc/Integral/integral_wd.con.
+inline "cic:/CoRN/ftc/Integral/integral_wd.con".
-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
@@ -196,41 +200,41 @@ Opaque Even_Partition.
The integral is a linear and monotonous function; in order to prove these facts we also need the important equalities $\int_a^bdx=b-a$#∫abdx=b-a# and $\int_a^af(x)dx=0$#∫aa=0#.
*)
-inline cic:/CoRN/ftc/Integral/integral_one.con.
+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.
+inline "cic:/CoRN/ftc/Integral/integral_comm_scal.con".
-inline cic:/CoRN/ftc/Integral/integral_plus.con.
+inline "cic:/CoRN/ftc/Integral/integral_plus.con".
(* UNEXPORTED
Transparent Even_Partition.
*)
-inline cic:/CoRN/ftc/Integral/integral_empty.con.
+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
@@ -238,72 +242,72 @@ 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.
+inline "cic:/CoRN/ftc/Integral/linear_integral.con".
(* UNEXPORTED
Opaque nring.
*)
-inline cic:/CoRN/ftc/Integral/monotonous_integral.con.
+inline "cic:/CoRN/ftc/Integral/monotonous_integral.con".
(* UNEXPORTED
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.
*)
-inline cic:/CoRN/ftc/Integral/integral_const.con.
+inline "cic:/CoRN/ftc/Integral/integral_const.con".
-inline cic:/CoRN/ftc/Integral/integral_minus.con.
+inline "cic:/CoRN/ftc/Integral/integral_minus.con".
-inline cic:/CoRN/ftc/Integral/integral_inv.con.
+inline "cic:/CoRN/ftc/Integral/integral_inv.con".
(*#*
We can also bound integrals by bounding the integrated functions.
*)
-inline cic:/CoRN/ftc/Integral/lb_integral.con.
+inline "cic:/CoRN/ftc/Integral/lb_integral.con".
-inline cic:/CoRN/ftc/Integral/ub_integral.con.
+inline "cic:/CoRN/ftc/Integral/ub_integral.con".
-inline cic:/CoRN/ftc/Integral/integral_leEq_norm.con.
+inline "cic:/CoRN/ftc/Integral/integral_leEq_norm.con".
(* UNEXPORTED
-End Corollaries.
+End Corollaries
*)
(* UNEXPORTED
-Section Integral_Sum.
+Section Integral_Sum
*)
(*#*
@@ -315,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
*)
(*#*
@@ -345,41 +349,41 @@ 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 *)
-inline cic:/CoRN/ftc/Integral/partition_join_aux.con.
+inline "cic:/CoRN/ftc/Integral/partition_join_aux.con".
(* end hide *)
-inline cic:/CoRN/ftc/Integral/partition_join_fun.con.
+inline "cic:/CoRN/ftc/Integral/partition_join_fun.con".
(* begin hide *)
-inline cic:/CoRN/ftc/Integral/pjf_1.con.
+inline "cic:/CoRN/ftc/Integral/pjf_1.con".
-inline cic:/CoRN/ftc/Integral/pjf_2.con.
+inline "cic:/CoRN/ftc/Integral/pjf_2.con".
-inline cic:/CoRN/ftc/Integral/pjf_2'.con.
+inline "cic:/CoRN/ftc/Integral/pjf_2'.con".
-inline cic:/CoRN/ftc/Integral/pjf_3.con.
+inline "cic:/CoRN/ftc/Integral/pjf_3.con".
-inline cic:/CoRN/ftc/Integral/partition_join_prf1.con.
+inline "cic:/CoRN/ftc/Integral/partition_join_prf1.con".
-inline cic:/CoRN/ftc/Integral/partition_join_prf2.con.
+inline "cic:/CoRN/ftc/Integral/partition_join_prf2.con".
-inline cic:/CoRN/ftc/Integral/partition_join_start.con.
+inline "cic:/CoRN/ftc/Integral/partition_join_start.con".
-inline cic:/CoRN/ftc/Integral/partition_join_finish.con.
+inline "cic:/CoRN/ftc/Integral/partition_join_finish.con".
-inline cic:/CoRN/ftc/Integral/partition_join.con.
+inline "cic:/CoRN/ftc/Integral/partition_join.con".
(* end hide *)
@@ -388,39 +392,39 @@ 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 *)
-inline cic:/CoRN/ftc/Integral/partition_join_aux'.con.
+inline "cic:/CoRN/ftc/Integral/partition_join_aux'.con".
(* end hide *)
-inline cic:/CoRN/ftc/Integral/partition_join_pts.con.
+inline "cic:/CoRN/ftc/Integral/partition_join_pts.con".
(* begin hide *)
-inline cic:/CoRN/ftc/Integral/pjp_1.con.
+inline "cic:/CoRN/ftc/Integral/pjp_1.con".
-inline cic:/CoRN/ftc/Integral/pjp_2.con.
+inline "cic:/CoRN/ftc/Integral/pjp_2.con".
-inline cic:/CoRN/ftc/Integral/pjp_3.con.
+inline "cic:/CoRN/ftc/Integral/pjp_3.con".
(* end hide *)
-inline cic:/CoRN/ftc/Integral/partition_join_Pts_in_partition.con.
+inline "cic:/CoRN/ftc/Integral/partition_join_Pts_in_partition.con".
-inline cic:/CoRN/ftc/Integral/partition_join_Pts_wd.con.
+inline "cic:/CoRN/ftc/Integral/partition_join_Pts_wd.con".
(* UNEXPORTED
Opaque partition_join.
@@ -446,12 +450,12 @@ Opaque minus.
Transparent minus.
*)
-inline cic:/CoRN/ftc/Integral/partition_join_Sum_lemma.con.
+inline "cic:/CoRN/ftc/Integral/partition_join_Sum_lemma.con".
-inline cic:/CoRN/ftc/Integral/partition_join_mesh.con.
+inline "cic:/CoRN/ftc/Integral/partition_join_mesh.con".
(* UNEXPORTED
-End Partition_Join.
+End Partition_Join
*)
(*#*
@@ -462,10 +466,10 @@ With these results in mind, the following is a trivial consequence:
Opaque Even_Partition.
*)
-inline cic:/CoRN/ftc/Integral/integral_plus_integral.con.
+inline "cic:/CoRN/ftc/Integral/integral_plus_integral.con".
(* UNEXPORTED
-End Integral_Sum.
+End Integral_Sum
*)
(* UNEXPORTED
@@ -473,18 +477,18 @@ Transparent Even_Partition.
*)
(* UNEXPORTED
-End Basic_Properties.
+End Basic_Properties
*)
(*#*
The following are simple consequences of this result and of previous ones.
*)
-inline cic:/CoRN/ftc/Integral/integral_less_norm.con.
+inline "cic:/CoRN/ftc/Integral/integral_less_norm.con".
(* end hide *)
-inline cic:/CoRN/ftc/Integral/integral_gt_zero.con.
+inline "cic:/CoRN/ftc/Integral/integral_gt_zero.con".
(* end hide *)