1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/ftc/Composition".
19 include "CoRN_notation.ma".
21 (* $Id: Composition.v,v 1.4 2004/04/23 10:00:58 lcf Exp $ *)
23 include "ftc/MoreFunctions.ma".
26 Section Maps_into_Compacts.
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
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.
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.
56 inline "cic:/CoRN/ftc/Composition/F.var".
58 inline "cic:/CoRN/ftc/Composition/G.var".
60 inline "cic:/CoRN/ftc/Composition/a.var".
62 inline "cic:/CoRN/ftc/Composition/b.var".
64 inline "cic:/CoRN/ftc/Composition/Hab.var".
66 inline "cic:/CoRN/ftc/Composition/c.var".
68 inline "cic:/CoRN/ftc/Composition/d.var".
70 inline "cic:/CoRN/ftc/Composition/Hcd.var".
74 inline "cic:/CoRN/ftc/Composition/I.con".
80 inline "cic:/CoRN/ftc/Composition/Hf.var".
84 inline "cic:/CoRN/ftc/Composition/maps_into_compacts.con".
88 inline "cic:/CoRN/ftc/Composition/maps.var".
92 inline "cic:/CoRN/ftc/Composition/maps_lemma'.con".
94 inline "cic:/CoRN/ftc/Composition/maps_lemma.con".
96 inline "cic:/CoRN/ftc/Composition/maps_lemma_less.con".
98 inline "cic:/CoRN/ftc/Composition/maps_lemma_inc.con".
105 End Maps_into_Compacts.
113 As was the case for division of partial functions, this condition
114 completely characterizes the domain of the composite function.
117 inline "cic:/CoRN/ftc/Composition/F.var".
119 inline "cic:/CoRN/ftc/Composition/G.var".
121 inline "cic:/CoRN/ftc/Composition/a.var".
123 inline "cic:/CoRN/ftc/Composition/b.var".
125 inline "cic:/CoRN/ftc/Composition/Hab.var".
127 inline "cic:/CoRN/ftc/Composition/c.var".
129 inline "cic:/CoRN/ftc/Composition/d.var".
131 inline "cic:/CoRN/ftc/Composition/Hcd.var".
135 inline "cic:/CoRN/ftc/Composition/Hf.var".
137 inline "cic:/CoRN/ftc/Composition/Hg.var".
139 inline "cic:/CoRN/ftc/Composition/maps.var".
143 inline "cic:/CoRN/ftc/Composition/included_comp.con".
150 Section Interval_Continuity.
155 We now prove that the composition of two continuous partial functions is continuous.
158 inline "cic:/CoRN/ftc/Composition/a.var".
160 inline "cic:/CoRN/ftc/Composition/b.var".
162 inline "cic:/CoRN/ftc/Composition/Hab.var".
166 inline "cic:/CoRN/ftc/Composition/I.con".
170 inline "cic:/CoRN/ftc/Composition/c.var".
172 inline "cic:/CoRN/ftc/Composition/d.var".
174 inline "cic:/CoRN/ftc/Composition/Hcd.var".
176 inline "cic:/CoRN/ftc/Composition/F.var".
178 inline "cic:/CoRN/ftc/Composition/G.var".
182 inline "cic:/CoRN/ftc/Composition/contF.var".
184 inline "cic:/CoRN/ftc/Composition/contG.var".
186 inline "cic:/CoRN/ftc/Composition/Hmap.var".
190 inline "cic:/CoRN/ftc/Composition/Continuous_I_comp.con".
193 End Interval_Continuity.
202 We now work with the derivative relation and prove the chain rule for partial functions.
205 inline "cic:/CoRN/ftc/Composition/F.var".
207 inline "cic:/CoRN/ftc/Composition/F'.var".
209 inline "cic:/CoRN/ftc/Composition/G.var".
211 inline "cic:/CoRN/ftc/Composition/G'.var".
213 inline "cic:/CoRN/ftc/Composition/a.var".
215 inline "cic:/CoRN/ftc/Composition/b.var".
217 inline "cic:/CoRN/ftc/Composition/Hab'.var".
219 inline "cic:/CoRN/ftc/Composition/c.var".
221 inline "cic:/CoRN/ftc/Composition/d.var".
223 inline "cic:/CoRN/ftc/Composition/Hcd'.var".
227 inline "cic:/CoRN/ftc/Composition/Hab.con".
229 inline "cic:/CoRN/ftc/Composition/Hcd.con".
231 inline "cic:/CoRN/ftc/Composition/I.con".
237 inline "cic:/CoRN/ftc/Composition/derF.var".
239 inline "cic:/CoRN/ftc/Composition/derG.var".
241 inline "cic:/CoRN/ftc/Composition/Hmap.var".
245 inline "cic:/CoRN/ftc/Composition/included_comp'.con".
247 inline "cic:/CoRN/ftc/Composition/maps'.con".
249 inline "cic:/CoRN/ftc/Composition/Derivative_I_comp.con".
252 The next lemma will be useful when we move on to differentiability.
255 inline "cic:/CoRN/ftc/Composition/Diffble_I_comp_aux.con".
262 Section Differentiability.
265 (*#* **Differentiability
267 Finally, we move on to differentiability.
270 inline "cic:/CoRN/ftc/Composition/F.var".
272 inline "cic:/CoRN/ftc/Composition/G.var".
274 inline "cic:/CoRN/ftc/Composition/a.var".
276 inline "cic:/CoRN/ftc/Composition/b.var".
278 inline "cic:/CoRN/ftc/Composition/Hab'.var".
280 inline "cic:/CoRN/ftc/Composition/c.var".
282 inline "cic:/CoRN/ftc/Composition/d.var".
284 inline "cic:/CoRN/ftc/Composition/Hcd'.var".
288 inline "cic:/CoRN/ftc/Composition/Hab.con".
290 inline "cic:/CoRN/ftc/Composition/Hcd.con".
292 inline "cic:/CoRN/ftc/Composition/I.con".
298 inline "cic:/CoRN/ftc/Composition/diffF.var".
300 inline "cic:/CoRN/ftc/Composition/diffG.var".
302 inline "cic:/CoRN/ftc/Composition/Hmap.var".
306 inline "cic:/CoRN/ftc/Composition/Diffble_I_comp.con".
309 End Differentiability.
313 Section Generalized_Intervals.
316 (*#* **Generalizations
318 We now generalize this results to arbitrary intervals. We begin by generalizing the notion of mapping compacts into compacts.
320 %\begin{convention}% We assume [I,J] to be proper intervals.
324 inline "cic:/CoRN/ftc/Composition/I.var".
326 inline "cic:/CoRN/ftc/Composition/J.var".
328 inline "cic:/CoRN/ftc/Composition/pI.var".
330 inline "cic:/CoRN/ftc/Composition/pJ.var".
332 inline "cic:/CoRN/ftc/Composition/maps_compacts_into.con".
335 Now everything comes naturally:
338 inline "cic:/CoRN/ftc/Composition/comp_inc_lemma.con".
340 inline "cic:/CoRN/ftc/Composition/F.var".
342 inline "cic:/CoRN/ftc/Composition/F'.var".
344 inline "cic:/CoRN/ftc/Composition/G.var".
346 inline "cic:/CoRN/ftc/Composition/G'.var".
350 inline "cic:/CoRN/ftc/Composition/Hmap.var".
354 inline "cic:/CoRN/ftc/Composition/Continuous_comp.con".
358 inline "cic:/CoRN/ftc/Composition/Hmap'.var".
362 inline "cic:/CoRN/ftc/Composition/Derivative_comp.con".
365 End Generalized_Intervals.
373 Finally, some criteria to prove that a function with a specific domain maps compacts into compacts:
376 inline "cic:/CoRN/ftc/Composition/positive_fun.con".
378 inline "cic:/CoRN/ftc/Composition/negative_fun.con".
380 inline "cic:/CoRN/ftc/Composition/positive_imp_maps_compacts_into.con".
382 inline "cic:/CoRN/ftc/Composition/negative_imp_maps_compacts_into.con".
384 inline "cic:/CoRN/ftc/Composition/Continuous_imp_maps_compacts_into.con".
387 As a corollary, we get the generalization of differentiability property.
390 inline "cic:/CoRN/ftc/Composition/Diffble_comp.con".
397 Hint Immediate included_comp: included.
401 Hint Immediate Continuous_I_comp Continuous_comp: continuous.