]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/CoRN-Decl/ftc/Composition.ma
two cases of cpx_lfxs_conf_fle closed
[helm.git] / matita / matita / contribs / CoRN-Decl / ftc / Composition.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/ftc/Composition".
18
19 include "CoRN.ma".
20
21 (* $Id: Composition.v,v 1.4 2004/04/23 10:00:58 lcf Exp $ *)
22
23 include "ftc/MoreFunctions.ma".
24
25 (* UNEXPORTED
26 Section Maps_into_Compacts
27 *)
28
29 (* UNEXPORTED
30 Section Part_Funct
31 *)
32
33 (*#* *Composition
34
35 Preservation results for functional composition are treated in this
36 separate file.  We start by defining some auxiliary predicates, and
37 then prove the preservation of continuity through composition and the
38 chain rule for differentiation, both for compact and arbitrary
39 intervals.
40
41 %\begin{convention}% Throughout this section:
42 - [a, b : IR] and [I] will denote [[a,b]];
43 - [c, d : IR] and [J] will denote [[c,d]];
44 - [F, F', G, G'] will be partial functions.
45
46 %\end{convention}%
47
48 ** Maps into Compacts
49
50 Both continuity and differentiability proofs require extra hypothesis
51 on the functions involved---namely, that every compact interval is
52 mapped into another compact interval.  We define this concept for
53 partial functions, and prove some trivial results.
54 *)
55
56 alias id "F" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/F.var".
57
58 alias id "G" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/G.var".
59
60 alias id "a" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/a.var".
61
62 alias id "b" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/b.var".
63
64 alias id "Hab" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hab.var".
65
66 alias id "c" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/c.var".
67
68 alias id "d" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/d.var".
69
70 alias id "Hcd" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hcd.var".
71
72 (* begin hide *)
73
74 inline "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/I.con" "Maps_into_Compacts__Part_Funct__".
75
76 (* end hide *)
77
78 (* begin show *)
79
80 alias id "Hf" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hf.var".
81
82 (* end show *)
83
84 inline "cic:/CoRN/ftc/Composition/maps_into_compacts.con".
85
86 (* begin show *)
87
88 alias id "maps" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/maps.var".
89
90 (* end show *)
91
92 inline "cic:/CoRN/ftc/Composition/maps_lemma'.con".
93
94 inline "cic:/CoRN/ftc/Composition/maps_lemma.con".
95
96 inline "cic:/CoRN/ftc/Composition/maps_lemma_less.con".
97
98 inline "cic:/CoRN/ftc/Composition/maps_lemma_inc.con".
99
100 (* UNEXPORTED
101 End Part_Funct
102 *)
103
104 (* UNEXPORTED
105 End Maps_into_Compacts
106 *)
107
108 (* UNEXPORTED
109 Section Mapping
110 *)
111
112 (*#*
113 As was the case for division of partial functions, this condition
114 completely characterizes the domain of the composite function.
115 *)
116
117 alias id "F" = "cic:/CoRN/ftc/Composition/Mapping/F.var".
118
119 alias id "G" = "cic:/CoRN/ftc/Composition/Mapping/G.var".
120
121 alias id "a" = "cic:/CoRN/ftc/Composition/Mapping/a.var".
122
123 alias id "b" = "cic:/CoRN/ftc/Composition/Mapping/b.var".
124
125 alias id "Hab" = "cic:/CoRN/ftc/Composition/Mapping/Hab.var".
126
127 alias id "c" = "cic:/CoRN/ftc/Composition/Mapping/c.var".
128
129 alias id "d" = "cic:/CoRN/ftc/Composition/Mapping/d.var".
130
131 alias id "Hcd" = "cic:/CoRN/ftc/Composition/Mapping/Hcd.var".
132
133 (* begin show *)
134
135 alias id "Hf" = "cic:/CoRN/ftc/Composition/Mapping/Hf.var".
136
137 alias id "Hg" = "cic:/CoRN/ftc/Composition/Mapping/Hg.var".
138
139 alias id "maps" = "cic:/CoRN/ftc/Composition/Mapping/maps.var".
140
141 (* end show *)
142
143 inline "cic:/CoRN/ftc/Composition/included_comp.con".
144
145 (* UNEXPORTED
146 End Mapping
147 *)
148
149 (* UNEXPORTED
150 Section Interval_Continuity
151 *)
152
153 (*#* **Continuity
154
155 We now prove that the composition of two continuous partial functions is continuous.
156 *)
157
158 alias id "a" = "cic:/CoRN/ftc/Composition/Interval_Continuity/a.var".
159
160 alias id "b" = "cic:/CoRN/ftc/Composition/Interval_Continuity/b.var".
161
162 alias id "Hab" = "cic:/CoRN/ftc/Composition/Interval_Continuity/Hab.var".
163
164 (* begin hide *)
165
166 inline "cic:/CoRN/ftc/Composition/Interval_Continuity/I.con" "Interval_Continuity__".
167
168 (* end hide *)
169
170 alias id "c" = "cic:/CoRN/ftc/Composition/Interval_Continuity/c.var".
171
172 alias id "d" = "cic:/CoRN/ftc/Composition/Interval_Continuity/d.var".
173
174 alias id "Hcd" = "cic:/CoRN/ftc/Composition/Interval_Continuity/Hcd.var".
175
176 alias id "F" = "cic:/CoRN/ftc/Composition/Interval_Continuity/F.var".
177
178 alias id "G" = "cic:/CoRN/ftc/Composition/Interval_Continuity/G.var".
179
180 (* begin show *)
181
182 alias id "contF" = "cic:/CoRN/ftc/Composition/Interval_Continuity/contF.var".
183
184 alias id "contG" = "cic:/CoRN/ftc/Composition/Interval_Continuity/contG.var".
185
186 alias id "Hmap" = "cic:/CoRN/ftc/Composition/Interval_Continuity/Hmap.var".
187
188 (* end show *)
189
190 inline "cic:/CoRN/ftc/Composition/Continuous_I_comp.con".
191
192 (* UNEXPORTED
193 End Interval_Continuity
194 *)
195
196 (* UNEXPORTED
197 Section Derivative
198 *)
199
200 (*#* **Derivative
201
202 We now work with the derivative relation and prove the chain rule for partial functions.
203 *)
204
205 alias id "F" = "cic:/CoRN/ftc/Composition/Derivative/F.var".
206
207 alias id "F'" = "cic:/CoRN/ftc/Composition/Derivative/F'.var".
208
209 alias id "G" = "cic:/CoRN/ftc/Composition/Derivative/G.var".
210
211 alias id "G'" = "cic:/CoRN/ftc/Composition/Derivative/G'.var".
212
213 alias id "a" = "cic:/CoRN/ftc/Composition/Derivative/a.var".
214
215 alias id "b" = "cic:/CoRN/ftc/Composition/Derivative/b.var".
216
217 alias id "Hab'" = "cic:/CoRN/ftc/Composition/Derivative/Hab'.var".
218
219 alias id "c" = "cic:/CoRN/ftc/Composition/Derivative/c.var".
220
221 alias id "d" = "cic:/CoRN/ftc/Composition/Derivative/d.var".
222
223 alias id "Hcd'" = "cic:/CoRN/ftc/Composition/Derivative/Hcd'.var".
224
225 (* begin hide *)
226
227 inline "cic:/CoRN/ftc/Composition/Derivative/Hab.con" "Derivative__".
228
229 inline "cic:/CoRN/ftc/Composition/Derivative/Hcd.con" "Derivative__".
230
231 inline "cic:/CoRN/ftc/Composition/Derivative/I.con" "Derivative__".
232
233 (* end hide *)
234
235 (* begin show *)
236
237 alias id "derF" = "cic:/CoRN/ftc/Composition/Derivative/derF.var".
238
239 alias id "derG" = "cic:/CoRN/ftc/Composition/Derivative/derG.var".
240
241 alias id "Hmap" = "cic:/CoRN/ftc/Composition/Derivative/Hmap.var".
242
243 (* end show *)
244
245 inline "cic:/CoRN/ftc/Composition/included_comp'.con".
246
247 inline "cic:/CoRN/ftc/Composition/maps'.con".
248
249 inline "cic:/CoRN/ftc/Composition/Derivative_I_comp.con".
250
251 (*#*
252 The next lemma will be useful when we move on to differentiability.
253 *)
254
255 inline "cic:/CoRN/ftc/Composition/Diffble_I_comp_aux.con".
256
257 (* UNEXPORTED
258 End Derivative
259 *)
260
261 (* UNEXPORTED
262 Section Differentiability
263 *)
264
265 (*#* **Differentiability
266
267 Finally, we move on to differentiability.
268 *)
269
270 alias id "F" = "cic:/CoRN/ftc/Composition/Differentiability/F.var".
271
272 alias id "G" = "cic:/CoRN/ftc/Composition/Differentiability/G.var".
273
274 alias id "a" = "cic:/CoRN/ftc/Composition/Differentiability/a.var".
275
276 alias id "b" = "cic:/CoRN/ftc/Composition/Differentiability/b.var".
277
278 alias id "Hab'" = "cic:/CoRN/ftc/Composition/Differentiability/Hab'.var".
279
280 alias id "c" = "cic:/CoRN/ftc/Composition/Differentiability/c.var".
281
282 alias id "d" = "cic:/CoRN/ftc/Composition/Differentiability/d.var".
283
284 alias id "Hcd'" = "cic:/CoRN/ftc/Composition/Differentiability/Hcd'.var".
285
286 (* begin hide *)
287
288 inline "cic:/CoRN/ftc/Composition/Differentiability/Hab.con" "Differentiability__".
289
290 inline "cic:/CoRN/ftc/Composition/Differentiability/Hcd.con" "Differentiability__".
291
292 inline "cic:/CoRN/ftc/Composition/Differentiability/I.con" "Differentiability__".
293
294 (* end hide *)
295
296 (* begin show *)
297
298 alias id "diffF" = "cic:/CoRN/ftc/Composition/Differentiability/diffF.var".
299
300 alias id "diffG" = "cic:/CoRN/ftc/Composition/Differentiability/diffG.var".
301
302 alias id "Hmap" = "cic:/CoRN/ftc/Composition/Differentiability/Hmap.var".
303
304 (* end show *)
305
306 inline "cic:/CoRN/ftc/Composition/Diffble_I_comp.con".
307
308 (* UNEXPORTED
309 End Differentiability
310 *)
311
312 (* UNEXPORTED
313 Section Generalized_Intervals
314 *)
315
316 (*#* **Generalizations
317
318 We now generalize this results to arbitrary intervals.  We begin by generalizing the notion of mapping compacts into compacts.
319
320 %\begin{convention}% We assume [I,J] to be proper intervals.
321 %\end{convention}%
322 *)
323
324 alias id "I" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/I.var".
325
326 alias id "J" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/J.var".
327
328 alias id "pI" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/pI.var".
329
330 alias id "pJ" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/pJ.var".
331
332 inline "cic:/CoRN/ftc/Composition/maps_compacts_into.con".
333
334 (*#*
335 Now everything comes naturally:
336 *)
337
338 inline "cic:/CoRN/ftc/Composition/comp_inc_lemma.con".
339
340 alias id "F" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/F.var".
341
342 alias id "F'" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/F'.var".
343
344 alias id "G" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/G.var".
345
346 alias id "G'" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/G'.var".
347
348 (* begin show *)
349
350 alias id "Hmap" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/Hmap.var".
351
352 (* end show *)
353
354 inline "cic:/CoRN/ftc/Composition/Continuous_comp.con".
355
356 (* begin show *)
357
358 alias id "Hmap'" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/Hmap'.var".
359
360 (* end show *)
361
362 inline "cic:/CoRN/ftc/Composition/Derivative_comp.con".
363
364 (* UNEXPORTED
365 End Generalized_Intervals
366 *)
367
368 (* UNEXPORTED
369 Section Corollaries
370 *)
371
372 (*#*
373 Finally, some criteria to prove that a function with a specific domain maps compacts into compacts:
374 *)
375
376 inline "cic:/CoRN/ftc/Composition/positive_fun.con".
377
378 inline "cic:/CoRN/ftc/Composition/negative_fun.con".
379
380 inline "cic:/CoRN/ftc/Composition/positive_imp_maps_compacts_into.con".
381
382 inline "cic:/CoRN/ftc/Composition/negative_imp_maps_compacts_into.con".
383
384 inline "cic:/CoRN/ftc/Composition/Continuous_imp_maps_compacts_into.con".
385
386 (*#*
387 As a corollary, we get the generalization of differentiability property.
388 *)
389
390 inline "cic:/CoRN/ftc/Composition/Diffble_comp.con".
391
392 (* UNEXPORTED
393 End Corollaries
394 *)
395
396 (* UNEXPORTED
397 Hint Immediate included_comp: included.
398 *)
399
400 (* UNEXPORTED
401 Hint Immediate Continuous_I_comp Continuous_comp: continuous.
402 *)
403