set "baseuri" "cic:/matita/CoRN-Decl/ftc/Partitions".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: Partitions.v,v 1.7 2004/04/23 10:01:00 lcf Exp $ *)
(*#* printing Partition_Sum %\ensuremath{\sum_P}% #∑<sub>P</sub># *)
(* UNEXPORTED
-Section Definitions.
+Section Definitions
*)
(*#* *Partitions
inline "cic:/CoRN/ftc/Partitions/Partition.ind".
-coercion "cic:/matita/CoRN-Decl/ftc/Partitions/Pts.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/ftc/Partitions/Pts.con 0 (* compounds *).
(*#* Two immediate consequences of this are that [ai [<=] aj] whenever
[i < j] and that [ai] is in [[a,b]] for all [i].
inline "cic:/CoRN/ftc/Partitions/Even_Partition.con".
(* UNEXPORTED
-Section Refinements.
+Section Refinements
*)
-inline "cic:/CoRN/ftc/Partitions/a.var".
+alias id "a" = "cic:/CoRN/ftc/Partitions/Definitions/Refinements/a.var".
-inline "cic:/CoRN/ftc/Partitions/b.var".
+alias id "b" = "cic:/CoRN/ftc/Partitions/Definitions/Refinements/b.var".
-inline "cic:/CoRN/ftc/Partitions/Hab.var".
+alias id "Hab" = "cic:/CoRN/ftc/Partitions/Definitions/Refinements/Hab.var".
-inline "cic:/CoRN/ftc/Partitions/m.var".
+alias id "m" = "cic:/CoRN/ftc/Partitions/Definitions/Refinements/m.var".
-inline "cic:/CoRN/ftc/Partitions/n.var".
+alias id "n" = "cic:/CoRN/ftc/Partitions/Definitions/Refinements/n.var".
-inline "cic:/CoRN/ftc/Partitions/P.var".
+alias id "P" = "cic:/CoRN/ftc/Partitions/Definitions/Refinements/P.var".
-inline "cic:/CoRN/ftc/Partitions/Q.var".
+alias id "Q" = "cic:/CoRN/ftc/Partitions/Definitions/Refinements/Q.var".
(*#*
We now define what it means for a partition [Q] to be a refinement of
inline "cic:/CoRN/ftc/Partitions/Partition_Sum.con".
(* UNEXPORTED
-End Refinements.
+End Refinements
*)
(* UNEXPORTED
%\end{convention}%
*)
-inline "cic:/CoRN/ftc/Partitions/a.var".
+alias id "a" = "cic:/CoRN/ftc/Partitions/Definitions/a.var".
-inline "cic:/CoRN/ftc/Partitions/b.var".
+alias id "b" = "cic:/CoRN/ftc/Partitions/Definitions/b.var".
-inline "cic:/CoRN/ftc/Partitions/Hab.var".
+alias id "Hab" = "cic:/CoRN/ftc/Partitions/Definitions/Hab.var".
(* begin hide *)
-inline "cic:/CoRN/ftc/Partitions/I.con".
+inline "cic:/CoRN/ftc/Partitions/Definitions/I.con" "Definitions__".
(* end hide *)
(* UNEXPORTED
-Section Getting_Points.
+Section Getting_Points
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/ftc/Partitions/m.var".
+alias id "m" = "cic:/CoRN/ftc/Partitions/Definitions/Getting_Points/m.var".
-inline "cic:/CoRN/ftc/Partitions/Q.var".
+alias id "Q" = "cic:/CoRN/ftc/Partitions/Definitions/Getting_Points/Q.var".
inline "cic:/CoRN/ftc/Partitions/Partition_imp_points.con".
inline "cic:/CoRN/ftc/Partitions/Partition_imp_points_2.con".
(* UNEXPORTED
-End Getting_Points.
+End Getting_Points
*)
(*#*
As a corollary, given any continuous function [F] and a natural number we have an immediate choice of a sum of [F] in [[a,b]].
*)
-inline "cic:/CoRN/ftc/Partitions/F.var".
+alias id "F" = "cic:/CoRN/ftc/Partitions/Definitions/F.var".
-inline "cic:/CoRN/ftc/Partitions/contF.var".
+alias id "contF" = "cic:/CoRN/ftc/Partitions/Definitions/contF.var".
inline "cic:/CoRN/ftc/Partitions/Even_Partition_Sum.con".
(* UNEXPORTED
-End Definitions.
+End Definitions
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section Lemmas.
+Section Lemmas
*)
(*#* ** Properties of the mesh
%\end{convention}%
*)
-inline "cic:/CoRN/ftc/Partitions/a.var".
+alias id "a" = "cic:/CoRN/ftc/Partitions/Lemmas/a.var".
-inline "cic:/CoRN/ftc/Partitions/b.var".
+alias id "b" = "cic:/CoRN/ftc/Partitions/Lemmas/b.var".
(* begin hide *)
-inline "cic:/CoRN/ftc/Partitions/I.con".
+inline "cic:/CoRN/ftc/Partitions/Lemmas/I.con" "Lemmas__".
(* end hide *)
-inline "cic:/CoRN/ftc/Partitions/Hab.var".
+alias id "Hab" = "cic:/CoRN/ftc/Partitions/Lemmas/Hab.var".
-inline "cic:/CoRN/ftc/Partitions/n.var".
+alias id "n" = "cic:/CoRN/ftc/Partitions/Lemmas/n.var".
-inline "cic:/CoRN/ftc/Partitions/P.var".
+alias id "P" = "cic:/CoRN/ftc/Partitions/Lemmas/P.var".
inline "cic:/CoRN/ftc/Partitions/Mesh_lemma.con".
inline "cic:/CoRN/ftc/Partitions/Mesh_leEq.con".
(* UNEXPORTED
-End Lemmas.
+End Lemmas
*)
(* UNEXPORTED
-Section Even_Partitions.
+Section Even_Partitions
*)
(*#* More technical stuff. Two equal partitions have the same mesh.
%\end{convention}%
*)
-inline "cic:/CoRN/ftc/Partitions/a.var".
+alias id "a" = "cic:/CoRN/ftc/Partitions/Even_Partitions/a.var".
-inline "cic:/CoRN/ftc/Partitions/b.var".
+alias id "b" = "cic:/CoRN/ftc/Partitions/Even_Partitions/b.var".
(* begin hide *)
-inline "cic:/CoRN/ftc/Partitions/I.con".
+inline "cic:/CoRN/ftc/Partitions/Even_Partitions/I.con" "Even_Partitions__".
(* end hide *)
-inline "cic:/CoRN/ftc/Partitions/Hab.var".
+alias id "Hab" = "cic:/CoRN/ftc/Partitions/Even_Partitions/Hab.var".
(*#*
An interesting property: in a partition, if [ai [<] aj] then [i < j].
Even partitions always have a common refinement.
*)
-inline "cic:/CoRN/ftc/Partitions/m.var".
+alias id "m" = "cic:/CoRN/ftc/Partitions/Even_Partitions/m.var".
-inline "cic:/CoRN/ftc/Partitions/n.var".
+alias id "n" = "cic:/CoRN/ftc/Partitions/Even_Partitions/n.var".
-inline "cic:/CoRN/ftc/Partitions/Hm.var".
+alias id "Hm" = "cic:/CoRN/ftc/Partitions/Even_Partitions/Hm.var".
-inline "cic:/CoRN/ftc/Partitions/Hn.var".
+alias id "Hn" = "cic:/CoRN/ftc/Partitions/Even_Partitions/Hn.var".
(* begin hide *)
-inline "cic:/CoRN/ftc/Partitions/P.con".
+inline "cic:/CoRN/ftc/Partitions/Even_Partitions/P.con" "Even_Partitions__".
-inline "cic:/CoRN/ftc/Partitions/Q.con".
+inline "cic:/CoRN/ftc/Partitions/Even_Partitions/Q.con" "Even_Partitions__".
(* end hide *)
inline "cic:/CoRN/ftc/Partitions/even_partition_refinement.con".
(* UNEXPORTED
-End Even_Partitions.
+End Even_Partitions
*)
(* UNEXPORTED
-Section More_Definitions.
+Section More_Definitions
*)
(*#* ** Separation
Some auxiliary definitions. A partition is said to be separated if all its points are distinct.
*)
-inline "cic:/CoRN/ftc/Partitions/a.var".
+alias id "a" = "cic:/CoRN/ftc/Partitions/More_Definitions/a.var".
-inline "cic:/CoRN/ftc/Partitions/b.var".
+alias id "b" = "cic:/CoRN/ftc/Partitions/More_Definitions/b.var".
-inline "cic:/CoRN/ftc/Partitions/Hab.var".
+alias id "Hab" = "cic:/CoRN/ftc/Partitions/More_Definitions/Hab.var".
inline "cic:/CoRN/ftc/Partitions/_Separated.con".
%\end{convention}%
*)
-inline "cic:/CoRN/ftc/Partitions/n.var".
+alias id "n" = "cic:/CoRN/ftc/Partitions/More_Definitions/n.var".
-inline "cic:/CoRN/ftc/Partitions/m.var".
+alias id "m" = "cic:/CoRN/ftc/Partitions/More_Definitions/m.var".
-inline "cic:/CoRN/ftc/Partitions/P.var".
+alias id "P" = "cic:/CoRN/ftc/Partitions/More_Definitions/P.var".
-inline "cic:/CoRN/ftc/Partitions/Q.var".
+alias id "Q" = "cic:/CoRN/ftc/Partitions/More_Definitions/Q.var".
inline "cic:/CoRN/ftc/Partitions/Separated.con".
(* UNEXPORTED
-End More_Definitions.
+End More_Definitions
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section Sep_Partitions.
+Section Sep_Partitions
*)
-inline "cic:/CoRN/ftc/Partitions/a.var".
+alias id "a" = "cic:/CoRN/ftc/Partitions/Sep_Partitions/a.var".
-inline "cic:/CoRN/ftc/Partitions/b.var".
+alias id "b" = "cic:/CoRN/ftc/Partitions/Sep_Partitions/b.var".
(* begin hide *)
-inline "cic:/CoRN/ftc/Partitions/I.con".
+inline "cic:/CoRN/ftc/Partitions/Sep_Partitions/I.con" "Sep_Partitions__".
(* end hide *)
-inline "cic:/CoRN/ftc/Partitions/Hab.var".
+alias id "Hab" = "cic:/CoRN/ftc/Partitions/Sep_Partitions/Hab.var".
(*#*
The antimesh of a separated partition is always positive.
inline "cic:/CoRN/ftc/Partitions/partition_less_imp_gt_zero.con".
(* UNEXPORTED
-End Sep_Partitions.
+End Sep_Partitions
*)