X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fmetrics%2FProd_Sub.ma;h=46746e6f4cdff8f26c97f0b8fb7ceae83e6c1a58;hb=c450c3c9c829a8bd436732c939511731558d292d;hp=c1a6e78edf701b6ee2cdebaecd6dd9e7d89192ff;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git
diff --git a/helm/software/matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma b/helm/software/matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma
index c1a6e78ed..46746e6f4 100644
--- a/helm/software/matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma
@@ -16,14 +16,14 @@
set "baseuri" "cic:/matita/CoRN-Decl/metrics/Prod_Sub".
+include "CoRN.ma".
+
(* $Id: Prod_Sub.v,v 1.4 2004/04/23 10:01:02 lcf Exp $ *)
-(* INCLUDE
-IR_CPMSpace
-*)
+include "metrics/IR_CPMSpace.ma".
(* UNEXPORTED
-Section prodpsmetrics.
+Section prodpsmetrics
*)
(*#* **Product-Pseudo-Metric-Spaces
@@ -37,22 +37,22 @@ This is %\emph{not}% #not# the one used to make the metric of
$\RR^{2}$ #IR2# out of the metric of $\RR$ #IR#.
*)
-inline cic:/CoRN/metrics/Prod_Sub/dprod0.con.
+inline "cic:/CoRN/metrics/Prod_Sub/dprod0.con".
-inline cic:/CoRN/metrics/Prod_Sub/dprod0_strext.con.
+inline "cic:/CoRN/metrics/Prod_Sub/dprod0_strext.con".
-inline cic:/CoRN/metrics/Prod_Sub/d_prod0.con.
+inline "cic:/CoRN/metrics/Prod_Sub/d_prod0.con".
-inline cic:/CoRN/metrics/Prod_Sub/prod0cpsmetricspace_is_CPsMetricSpace.con.
+inline "cic:/CoRN/metrics/Prod_Sub/prod0cpsmetricspace_is_CPsMetricSpace.con".
-inline cic:/CoRN/metrics/Prod_Sub/Prod0CPsMetricSpace.con.
+inline "cic:/CoRN/metrics/Prod_Sub/Prod0CPsMetricSpace.con".
(* UNEXPORTED
-End prodpsmetrics.
+End prodpsmetrics
*)
(* UNEXPORTED
-Section subpsmetrics.
+Section subpsmetrics
*)
(*#* **Sub-Pseudo-Metric-Spaces
@@ -63,45 +63,45 @@ The pseudo metric on a subspace $Y$ #Y# of a pseudo metric space $X$ #X# is
the pseudo metric on $X$ #X# restricted to $Y$ #Y#.
*)
-inline cic:/CoRN/metrics/Prod_Sub/restr_bin_fun.con.
+inline "cic:/CoRN/metrics/Prod_Sub/restr_bin_fun.con".
(* UNEXPORTED
Implicit Arguments restr_bin_fun [X].
*)
-inline cic:/CoRN/metrics/Prod_Sub/restr_bin_fun'.con.
+inline "cic:/CoRN/metrics/Prod_Sub/restr_bin_fun'.con".
(* UNEXPORTED
Implicit Arguments restr_bin_fun' [X].
*)
-inline cic:/CoRN/metrics/Prod_Sub/restr_bin_fun_strext.con.
+inline "cic:/CoRN/metrics/Prod_Sub/restr_bin_fun_strext.con".
-inline cic:/CoRN/metrics/Prod_Sub/Build_SubCSetoid_bin_fun.con.
+inline "cic:/CoRN/metrics/Prod_Sub/Build_SubCSetoid_bin_fun.con".
-inline cic:/CoRN/metrics/Prod_Sub/dsub.con.
+inline "cic:/CoRN/metrics/Prod_Sub/dsub.con".
(* UNEXPORTED
Implicit Arguments dsub [X].
*)
-inline cic:/CoRN/metrics/Prod_Sub/dsub_com.con.
+inline "cic:/CoRN/metrics/Prod_Sub/dsub_com.con".
-inline cic:/CoRN/metrics/Prod_Sub/dsub_nneg.con.
+inline "cic:/CoRN/metrics/Prod_Sub/dsub_nneg.con".
-inline cic:/CoRN/metrics/Prod_Sub/dsub_pos_imp_ap.con.
+inline "cic:/CoRN/metrics/Prod_Sub/dsub_pos_imp_ap.con".
-inline cic:/CoRN/metrics/Prod_Sub/dsub_tri_ineq.con.
+inline "cic:/CoRN/metrics/Prod_Sub/dsub_tri_ineq.con".
-inline cic:/CoRN/metrics/Prod_Sub/is_SubPsMetricSpace.con.
+inline "cic:/CoRN/metrics/Prod_Sub/is_SubPsMetricSpace.con".
-inline cic:/CoRN/metrics/Prod_Sub/SubPsMetricSpace.con.
+inline "cic:/CoRN/metrics/Prod_Sub/SubPsMetricSpace.con".
(* UNEXPORTED
Implicit Arguments SubPsMetricSpace [X].
*)
-inline cic:/CoRN/metrics/Prod_Sub/from_SubPsMetricSpace.con.
+inline "cic:/CoRN/metrics/Prod_Sub/from_SubPsMetricSpace.con".
(*#*
The function [dsub'] is used in the definition of %''located''% #"located"#.
@@ -109,23 +109,23 @@ It enables one to speak about a distance between an element of a
pseudo metric space and a certain subspace.
*)
-inline cic:/CoRN/metrics/Prod_Sub/dsub'.con.
+inline "cic:/CoRN/metrics/Prod_Sub/dsub'.con".
(* UNEXPORTED
Implicit Arguments dsub' [X].
*)
-inline cic:/CoRN/metrics/Prod_Sub/dsub'_strext.con.
+inline "cic:/CoRN/metrics/Prod_Sub/dsub'_strext.con".
-inline cic:/CoRN/metrics/Prod_Sub/dsub'_as_cs_fun.con.
+inline "cic:/CoRN/metrics/Prod_Sub/dsub'_as_cs_fun.con".
(* UNEXPORTED
Implicit Arguments dsub'_as_cs_fun [X].
*)
-inline cic:/CoRN/metrics/Prod_Sub/dsub'_uni_continuous''.con.
+inline "cic:/CoRN/metrics/Prod_Sub/dsub'_uni_continuous''.con".
(* UNEXPORTED
-End subpsmetrics.
+End subpsmetrics
*)