]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/procedural/CoRN/metrics/ContFunctions.mma
Stuff moved from old Matita.
[helm.git] / matita / matita / contribs / procedural / CoRN / metrics / ContFunctions.mma
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 include "CoRN.ma".
18
19 (* $Id: ContFunctions.v,v 1.3 2004/04/23 10:01:02 lcf Exp $ *)
20
21 include "metrics/CPseudoMSpaces.ma".
22
23 (* UNEXPORTED
24 Section Continuous_functions
25 *)
26
27 (*#* **Continuous functions, uniformly continuous functions and Lipschitz functions
28 %\begin{convention}%
29 Let [A] and [B] be pseudo metric spaces.
30 %\end{convention}%
31 *)
32
33 (* UNEXPORTED
34 cic:/CoRN/metrics/ContFunctions/Continuous_functions/A.var
35 *)
36
37 (* UNEXPORTED
38 cic:/CoRN/metrics/ContFunctions/Continuous_functions/B.var
39 *)
40
41 (*#*
42 We will look at some notions of continuous functions.
43 *)
44
45 inline procedural "cic:/CoRN/metrics/ContFunctions/continuous.con" as definition.
46
47 inline procedural "cic:/CoRN/metrics/ContFunctions/continuous'.con" as definition.
48
49 inline procedural "cic:/CoRN/metrics/ContFunctions/uni_continuous.con" as definition.
50
51 inline procedural "cic:/CoRN/metrics/ContFunctions/uni_continuous'.con" as definition.
52
53 inline procedural "cic:/CoRN/metrics/ContFunctions/uni_continuous''.con" as definition.
54
55 inline procedural "cic:/CoRN/metrics/ContFunctions/lipschitz.con" as definition.
56
57 inline procedural "cic:/CoRN/metrics/ContFunctions/lipschitz'.con" as definition.
58
59 (* UNEXPORTED
60 End Continuous_functions
61 *)
62
63 (* UNEXPORTED
64 Implicit Arguments continuous [A B].
65 *)
66
67 (* UNEXPORTED
68 Implicit Arguments uni_continuous [A B].
69 *)
70
71 (* UNEXPORTED
72 Implicit Arguments lipschitz [A B].
73 *)
74
75 (* UNEXPORTED
76 Implicit Arguments continuous' [A B].
77 *)
78
79 (* UNEXPORTED
80 Implicit Arguments uni_continuous' [A B].
81 *)
82
83 (* UNEXPORTED
84 Implicit Arguments uni_continuous'' [A B].
85 *)
86
87 (* UNEXPORTED
88 Implicit Arguments lipschitz' [A B].
89 *)
90
91 (* UNEXPORTED
92 Section Lemmas
93 *)
94
95 (* begin hide *)
96
97 inline procedural "cic:/CoRN/metrics/ContFunctions/nexp_power.con" as lemma.
98
99 (* end hide *)
100
101 inline procedural "cic:/CoRN/metrics/ContFunctions/continuous_imp_continuous'.con" as lemma.
102
103 inline procedural "cic:/CoRN/metrics/ContFunctions/continuous'_imp_continuous.con" as lemma.
104
105 inline procedural "cic:/CoRN/metrics/ContFunctions/uni_continuous_imp_uni_continuous'.con" as lemma.
106
107 inline procedural "cic:/CoRN/metrics/ContFunctions/uni_continuous'_imp_uni_continuous.con" as lemma.
108
109 inline procedural "cic:/CoRN/metrics/ContFunctions/uni_continuous'_imp_uni_continuous''.con" as lemma.
110
111 inline procedural "cic:/CoRN/metrics/ContFunctions/lipschitz_imp_lipschitz'.con" as lemma.
112
113 inline procedural "cic:/CoRN/metrics/ContFunctions/lipschitz'_imp_lipschitz.con" as lemma.
114
115 (*#*
116 Every uniformly continuous function is continuous and 
117 every Lipschitz function is uniformly continuous.
118 *)
119
120 inline procedural "cic:/CoRN/metrics/ContFunctions/uni_continuous_imp_continuous.con" as lemma.
121
122 inline procedural "cic:/CoRN/metrics/ContFunctions/lipschitz_imp_uni_continuous.con" as lemma.
123
124 (* UNEXPORTED
125 End Lemmas
126 *)
127
128 (* UNEXPORTED
129 Section Identity
130 *)
131
132 (*#* **Identity 
133 *)
134
135 (*#*
136 The identity function is Lipschitz. 
137 Hence it is uniformly continuous and continuous.
138 *)
139
140 inline procedural "cic:/CoRN/metrics/ContFunctions/id_is_lipschitz.con" as lemma.
141
142 inline procedural "cic:/CoRN/metrics/ContFunctions/id_is_uni_continuous.con" as lemma.
143
144 inline procedural "cic:/CoRN/metrics/ContFunctions/id_is_continuous.con" as lemma.
145
146 (* UNEXPORTED
147 End Identity
148 *)
149
150 (* UNEXPORTED
151 Section Constant
152 *)
153
154 (*#* **Constant functions
155 %\begin{convention}%
156 Let [B] and [X] be pseudo metric spaces.
157 %\end{convention}%
158 *)
159
160 (*#*
161 Any constant function is Lipschitz. 
162 Hence it is uniformly continuous and continuous.
163 *)
164
165 (* UNEXPORTED
166 cic:/CoRN/metrics/ContFunctions/Constant/B.var
167 *)
168
169 (* UNEXPORTED
170 cic:/CoRN/metrics/ContFunctions/Constant/X.var
171 *)
172
173 inline procedural "cic:/CoRN/metrics/ContFunctions/const_fun_is_lipschitz.con" as lemma.
174
175 inline procedural "cic:/CoRN/metrics/ContFunctions/const_fun_is_uni_continuous.con" as lemma.
176
177 inline procedural "cic:/CoRN/metrics/ContFunctions/const_fun_is_continuous.con" as lemma.
178
179 (* UNEXPORTED
180 End Constant
181 *)
182
183 (* UNEXPORTED
184 Section Composition
185 *)
186
187 (*#* **Composition
188 %\begin{convention}%
189 Let [B],[C] and [X] be pseudo metric spaces.
190 Let [f : (CSetoid_fun X B)] and
191 [g : (CSetoid_fun  B C)].
192 %\end{convention}%
193 *)
194
195 (*#*
196 The composition of two Lipschitz/uniformly continous/continuous functions is 
197 again Lipschitz/uniformly continuous/continuous.
198 *)
199
200 (* UNEXPORTED
201 cic:/CoRN/metrics/ContFunctions/Composition/X.var
202 *)
203
204 (* UNEXPORTED
205 cic:/CoRN/metrics/ContFunctions/Composition/B.var
206 *)
207
208 (* UNEXPORTED
209 cic:/CoRN/metrics/ContFunctions/Composition/f.var
210 *)
211
212 (* UNEXPORTED
213 cic:/CoRN/metrics/ContFunctions/Composition/C.var
214 *)
215
216 (* UNEXPORTED
217 cic:/CoRN/metrics/ContFunctions/Composition/g.var
218 *)
219
220 inline procedural "cic:/CoRN/metrics/ContFunctions/comp_resp_lipschitz.con" as lemma.
221
222 inline procedural "cic:/CoRN/metrics/ContFunctions/comp_resp_uni_continuous.con" as lemma.
223
224 inline procedural "cic:/CoRN/metrics/ContFunctions/comp_resp_continuous.con" as lemma.
225
226 (* UNEXPORTED
227 End Composition
228 *)
229
230 (* UNEXPORTED
231 Section Limit
232 *)
233
234 (*#* **Limit
235 *)
236
237 inline procedural "cic:/CoRN/metrics/ContFunctions/MSseqLimit.con" as definition.
238
239 (* UNEXPORTED
240 Implicit Arguments MSseqLimit [X].
241 *)
242
243 inline procedural "cic:/CoRN/metrics/ContFunctions/MSseqLimit'.con" as definition.
244
245 (* UNEXPORTED
246 Implicit Arguments MSseqLimit' [X].
247 *)
248
249 inline procedural "cic:/CoRN/metrics/ContFunctions/MSseqLimit_imp_MSseqLimit'.con" as lemma.
250
251 inline procedural "cic:/CoRN/metrics/ContFunctions/MSseqLimit'_imp_MSseqLimit.con" as lemma.
252
253 inline procedural "cic:/CoRN/metrics/ContFunctions/seqcontinuous'.con" as definition.
254
255 (* UNEXPORTED
256 Implicit Arguments seqcontinuous' [A B].
257 *)
258
259 inline procedural "cic:/CoRN/metrics/ContFunctions/continuous'_imp_seqcontinuous'.con" as lemma.
260
261 (* UNEXPORTED
262 End Limit
263 *)
264