]> matita.cs.unibo.it Git - helm.git/blob - matita/contribs/CoRN-Decl/metrics/CPseudoMSpaces.ma
librarySync - we do not generate the object attributes when we publish the xml
[helm.git] / matita / contribs / CoRN-Decl / metrics / CPseudoMSpaces.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 set "baseuri" "cic:/matita/CoRN-Decl/metrics/CPseudoMSpaces".
18
19 include "CoRN.ma".
20
21 (* $Id: CPseudoMSpaces.v,v 1.3 2004/04/23 10:01:02 lcf Exp $ *)
22
23 include "reals/Intervals.ma".
24
25 (*#* *Metric Spaces
26 *)
27
28 (* UNEXPORTED
29 Section Relations
30 *)
31
32 (*#* **Relations necessary for Pseudo Metric Spaces and Metric Spaces
33 %\begin{convention}%
34 Let [A : CSetoid], [d : (CSetoid_bin_fun A A IR)].
35 %\end{convention}%
36 *)
37
38 alias id "A" = "cic:/CoRN/metrics/CPseudoMSpaces/Relations/A.var".
39
40 alias id "d" = "cic:/CoRN/metrics/CPseudoMSpaces/Relations/d.var".
41
42 (* UNEXPORTED
43 Set Implicit Arguments.
44 *)
45
46 (* UNEXPORTED
47 Unset Strict Implicit.
48 *)
49
50 inline "cic:/CoRN/metrics/CPseudoMSpaces/com.con".
51
52 inline "cic:/CoRN/metrics/CPseudoMSpaces/nneg.con".
53
54 inline "cic:/CoRN/metrics/CPseudoMSpaces/pos_imp_ap.con".
55
56 inline "cic:/CoRN/metrics/CPseudoMSpaces/tri_ineq.con".
57
58 (* UNEXPORTED
59 Set Strict Implicit.
60 *)
61
62 (* UNEXPORTED
63 Unset Implicit Arguments.
64 *)
65
66 inline "cic:/CoRN/metrics/CPseudoMSpaces/diag_zero.con".
67
68 inline "cic:/CoRN/metrics/CPseudoMSpaces/apdiag_imp_grzero.con".
69
70 (* UNEXPORTED
71 End Relations
72 *)
73
74 (* UNEXPORTED
75 Section Definition_PsMS0
76 *)
77
78 (*#* **Definition of Pseudo Metric Space
79 *)
80
81 (*#*
82 A pseudo metric space consists of a setoid and a %''pseudo metric''% #"pseudo metric"#, also called
83 %''distance''% #"distance"#, a binairy function that fulfils certain properties.
84 *)
85
86 inline "cic:/CoRN/metrics/CPseudoMSpaces/is_CPsMetricSpace.ind".
87
88 inline "cic:/CoRN/metrics/CPseudoMSpaces/CPsMetricSpace.ind".
89
90 coercion cic:/matita/CoRN-Decl/metrics/CPseudoMSpaces/cms_crr.con 0 (* compounds *).
91
92 (* UNEXPORTED
93 End Definition_PsMS0
94 *)
95
96 (* UNEXPORTED
97 Implicit Arguments cms_d [c].
98 *)
99
100 (* NOTATION
101 Infix "[-d]" := cms_d (at level 68, left associativity).
102 *)
103
104 (* UNEXPORTED
105 Section PsMS_axioms
106 *)
107
108 (*#* **Pseudo Metric Space axioms
109 %\begin{convention}%
110 Let [A] be a pseudo metric space.
111 %\end{convention}%
112 *)
113
114 alias id "A" = "cic:/CoRN/metrics/CPseudoMSpaces/PsMS_axioms/A.var".
115
116 inline "cic:/CoRN/metrics/CPseudoMSpaces/CPsMetricSpace_is_CPsMetricSpace.con".
117
118 inline "cic:/CoRN/metrics/CPseudoMSpaces/d_com.con".
119
120 inline "cic:/CoRN/metrics/CPseudoMSpaces/d_nneg.con".
121
122 inline "cic:/CoRN/metrics/CPseudoMSpaces/d_pos_imp_ap.con".
123
124 inline "cic:/CoRN/metrics/CPseudoMSpaces/d_tri_ineq.con".
125
126 (* UNEXPORTED
127 End PsMS_axioms
128 *)
129
130 (* UNEXPORTED
131 Section PsMS_basics
132 *)
133
134 (*#* **Pseudo Metric Space basics
135 %\begin{convention}%
136 Let [Y] be a pseudo metric space.
137 %\end{convention}%
138 *)
139
140 alias id "Y" = "cic:/CoRN/metrics/CPseudoMSpaces/PsMS_basics/Y.var".
141
142 inline "cic:/CoRN/metrics/CPseudoMSpaces/rev_tri_ineq.con".
143
144 (*#*
145 Instead of taking [pos_imp_ap] as axiom, 
146 we could as well have taken [diag_zero]. 
147 *)
148
149 inline "cic:/CoRN/metrics/CPseudoMSpaces/diag_zero_imp_pos_imp_ap.con".
150
151 inline "cic:/CoRN/metrics/CPseudoMSpaces/pos_imp_ap_imp_diag_zero.con".
152
153 inline "cic:/CoRN/metrics/CPseudoMSpaces/is_CPsMetricSpace_diag_zero.con".
154
155 (* UNEXPORTED
156 End PsMS_basics
157 *)
158
159 (* UNEXPORTED
160 Section Zerof
161 *)
162
163 (*#* **Zero function
164 *)
165
166 (*#*
167 Every setoid forms with the binary function that always returns zero, 
168 a pseudo metric space. 
169 *)
170
171 inline "cic:/CoRN/metrics/CPseudoMSpaces/zero_fun.con".
172
173 inline "cic:/CoRN/metrics/CPseudoMSpaces/zero_fun_strext.con".
174
175 inline "cic:/CoRN/metrics/CPseudoMSpaces/Zero_fun.con".
176
177 inline "cic:/CoRN/metrics/CPseudoMSpaces/zero_fun_com.con".
178
179 inline "cic:/CoRN/metrics/CPseudoMSpaces/zero_fun_nneg.con".
180
181 inline "cic:/CoRN/metrics/CPseudoMSpaces/zero_fun_pos_imp_ap.con".
182
183 inline "cic:/CoRN/metrics/CPseudoMSpaces/zero_fun_tri_ineq.con".
184
185 inline "cic:/CoRN/metrics/CPseudoMSpaces/zf_is_CPsMetricSpace.con".
186
187 inline "cic:/CoRN/metrics/CPseudoMSpaces/zf_as_CPsMetricSpace.con".
188
189 (* UNEXPORTED
190 End Zerof
191 *)
192