]> matita.cs.unibo.it Git - helm.git/blob - matita/contribs/CoRN-Decl/ftc/RefLemma.ma
librarySync - we do not generate the object attributes when we publish the xml
[helm.git] / matita / contribs / CoRN-Decl / ftc / RefLemma.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/RefLemma".
18
19 include "CoRN.ma".
20
21 (* $Id: RefLemma.v,v 1.7 2004/04/23 10:01:00 lcf Exp $ *)
22
23 include "ftc/RefSeparating.ma".
24
25 include "ftc/RefSeparated.ma".
26
27 include "ftc/RefSepRef.ma".
28
29 (* UNEXPORTED
30 Section Refinement_Lemma
31 *)
32
33 (*#* *The Refinement Lemmas
34
35 Here we resume the results proved in four different files.  The aim is to prove the following result (last part of Theorem 2.9 of Bishop 1967):
36
37 %\noindent\textbf{%#<b>#Theorem#</b>#%}% Let [f] be a continuous function on a
38 compact interval [[a,b]] with modulus of continuity%\footnote{%# (#From our
39 point of view, the modulus of continuity is simply the proof that [f] is
40 continuous.#)#%}% [omega].
41 Let [P] be a partition of [[a,b]] and [eps [>] Zero] be such that
42 [mesh(P)  [<]  omega(eps)].
43 Then
44 %\[\left|S(f,P)-\int_a^bf(x)dx\right|\leq\varepsilon(b-a),\]%#|S(f,P)-&int;f(x)dx|&le;&epsilon;(b-a)#
45 where [S(f,P)] denotes any sum of the function [f] respecting the partition
46 [P] (as previously defined).
47
48 The proof of this theorem relies on the fact that for any two partitions [P]
49 and [R] of [[a,b]] it is possible to define a partition [Q] which is
50 ``almost'' a common refinement of [P] and [R]---that is, given [eps [>] Zero]
51 it is possible to define [Q] such that for every point [x] of either [P] or
52 [R] there is a point [y] of [Q] such that [|x[-]y|  [<]  eps].
53 This requires three separate constructions (done in three separate files)
54 which are then properly combined to give the final result.  We recommend the
55 reader to ignore this technical constructions.
56
57 First we prove that if [P] and [R] are both
58 separated (though not necessarily separated from each other) then we can
59 define a partition [P'] arbitrarily close to [P] (that is, such that given
60 [alpha [>] Zero] and [xi [>] Zero] [P'] satisfies both
61 [mesh(P')  [<]  mesh(P) [+] xi] and for every choice of points [x_i] respecting
62 [P] there is a choice of points [x'_i] respecting [P'] such that
63 [|S(f,P)-S(f,P')|  [<]  alpha]) that is separated from [R].
64
65 Then we prove that given any partition [P]
66 and assuming [a  [#]  b] we can define a partition [P'] arbitrarily close to
67 [P] (in the same sense as above) which is separated.
68
69 Finally we prove that every two separated
70 partitions [P] and [R] have a common refinement---as every two points in [P]
71 and [R] are apart, we can decide which one is smaller.  We use here the
72 technical results about ordering that we proved in the file [IntegralLemmas.v].
73
74 Using the results from these files, we prove our main lemma in several steps
75 (and versions).
76
77 %\begin{convention}% Throughout this section:
78  - [a,b:IR] and [I] denotes [[a,b]];
79  - [F] is a partial function continuous in [I].
80
81 %\end{convention}%
82 *)
83
84 alias id "a" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/a.var".
85
86 alias id "b" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/b.var".
87
88 alias id "Hab" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Hab.var".
89
90 (* begin hide *)
91
92 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/I.con" "Refinement_Lemma__".
93
94 (* end hide *)
95
96 alias id "F" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/F.var".
97
98 alias id "contF" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/contF.var".
99
100 alias id "incF" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/incF.var".
101
102 (* begin hide *)
103
104 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/contF'.con" "Refinement_Lemma__".
105
106 (* end hide *)
107
108 (* UNEXPORTED
109 Section First_Refinement_Lemma
110 *)
111
112 (*#*
113 This is the first part of the proof of Theorem 2.9.
114
115 %\begin{convention}%
116  - [P, Q] are partitions of [I] with, respectively, [n] and [m] points;
117  - [Q] is a refinement of [P];
118  - [e] is a positive real number;
119  - [d] is the modulus of continuity of [F] for [e];
120  - the mesh of [P] is less or equal to [d];
121  - [fP] and [fQ] are choices of points respecting the partitions [P] and [Q],
122 respectively.
123
124 %\end{convention}%
125 *)
126
127 alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/e.var".
128
129 alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/He.var".
130
131 (* begin hide *)
132
133 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/d.con" "Refinement_Lemma__First_Refinement_Lemma__".
134
135 (* end hide *)
136
137 alias id "m" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/m.var".
138
139 alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/n.var".
140
141 alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/P.var".
142
143 alias id "HMesh" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HMesh.var".
144
145 alias id "Q" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/Q.var".
146
147 alias id "Href" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/Href.var".
148
149 alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/fP.var".
150
151 alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfP.var".
152
153 alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfP'.var".
154
155 alias id "fQ" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/fQ.var".
156
157 alias id "HfQ" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfQ.var".
158
159 alias id "HfQ'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfQ'.var".
160
161 (* begin hide *)
162
163 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/sub.con" "Refinement_Lemma__First_Refinement_Lemma__".
164
165 inline "cic:/CoRN/ftc/RefLemma/RL_sub_0.con".
166
167 inline "cic:/CoRN/ftc/RefLemma/RL_sub_n.con".
168
169 inline "cic:/CoRN/ftc/RefLemma/RL_sub_mon.con".
170
171 inline "cic:/CoRN/ftc/RefLemma/RL_sub_mon'.con".
172
173 inline "cic:/CoRN/ftc/RefLemma/RL_sub_hyp.con".
174
175 inline "cic:/CoRN/ftc/RefLemma/RL_sub_S.con".
176
177 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H.con" "Refinement_Lemma__First_Refinement_Lemma__".
178
179 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H'.con" "Refinement_Lemma__First_Refinement_Lemma__".
180
181 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H0.con" "Refinement_Lemma__First_Refinement_Lemma__".
182
183 inline "cic:/CoRN/ftc/RefLemma/RL_sub_SS.con".
184
185 inline "cic:/CoRN/ftc/RefLemma/RL_h.con".
186
187 inline "cic:/CoRN/ftc/RefLemma/RL_g.con".
188
189 (* NOTATION
190 Notation g := RL_g.
191 *)
192
193 (* NOTATION
194 Notation h := RL_h.
195 *)
196
197 inline "cic:/CoRN/ftc/RefLemma/ref_calc1.con".
198
199 (* NOTATION
200 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfP _ _)).
201 *)
202
203 (* NOTATION
204 Notation just2 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfQ _ _)).
205 *)
206
207 inline "cic:/CoRN/ftc/RefLemma/ref_calc2.con".
208
209 inline "cic:/CoRN/ftc/RefLemma/ref_calc3.con".
210
211 inline "cic:/CoRN/ftc/RefLemma/ref_calc4.con".
212
213 inline "cic:/CoRN/ftc/RefLemma/ref_calc5.con".
214
215 inline "cic:/CoRN/ftc/RefLemma/ref_calc6.con".
216
217 inline "cic:/CoRN/ftc/RefLemma/ref_calc7.con".
218
219 inline "cic:/CoRN/ftc/RefLemma/ref_calc8.con".
220
221 (* end hide *)
222
223 inline "cic:/CoRN/ftc/RefLemma/first_refinement_lemma.con".
224
225 (* UNEXPORTED
226 End First_Refinement_Lemma
227 *)
228
229 (* UNEXPORTED
230 Section Second_Refinement_Lemma
231 *)
232
233 (*#*
234 This is inequality (2.6.7).
235
236 %\begin{convention}%
237  - [P, Q, R] are partitions of [I] with, respectively, [j, n] and [k] points;
238  - [Q] is a common refinement of [P] and [R];
239  - [e, e'] are positive real numbers;
240  - [d, d'] are the moduli of continuity of [F] for [e, e'];
241  - the Mesh of [P] is less or equal to [d];
242  - the Mesh of [R] is less or equal to [d'];
243  - [fP, fQ] and [fR] are choices of points respecting the partitions [P, Q]
244 and [R], respectively.
245
246 %\end{convention}%
247 *)
248
249 alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/n.var".
250
251 alias id "j" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/j.var".
252
253 alias id "k" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/k.var".
254
255 alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/P.var".
256
257 alias id "Q" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/Q.var".
258
259 alias id "R" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/R.var".
260
261 alias id "HrefP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HrefP.var".
262
263 alias id "HrefR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HrefR.var".
264
265 alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/e.var".
266
267 alias id "e'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/e'.var".
268
269 alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/He.var".
270
271 alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/He'.var".
272
273 (* begin hide *)
274
275 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/d.con" "Refinement_Lemma__Second_Refinement_Lemma__".
276
277 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/d'.con" "Refinement_Lemma__Second_Refinement_Lemma__".
278
279 (* end hide *)
280
281 alias id "HMeshP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HMeshP.var".
282
283 alias id "HMeshR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HMeshR.var".
284
285 alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/fP.var".
286
287 alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfP.var".
288
289 alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfP'.var".
290
291 alias id "fR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/fR.var".
292
293 alias id "HfR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfR.var".
294
295 alias id "HfR'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfR'.var".
296
297 inline "cic:/CoRN/ftc/RefLemma/second_refinement_lemma.con".
298
299 (* UNEXPORTED
300 End Second_Refinement_Lemma
301 *)
302
303 (* UNEXPORTED
304 Section Third_Refinement_Lemma
305 *)
306
307 (*#*
308 This is an approximation of inequality (2.6.7), but without assuming the existence of a common refinement of [P] and [R].
309
310 %\begin{convention}%
311  - [P, R] are partitions of [I] with, respectively, [n] and [m] points;
312  - [e, e'] are positive real numbers;
313  - [d, d'] are the moduli of continuity of [F] for [e, e'];
314  - the Mesh of [P] is less than [d];
315  - the Mesh of [R] is less than [d'];
316  - [fP] and [fR] are choices of points respecting the partitions [P] and [R],
317 respectively;
318  - [beta] is a positive real number.
319
320 %\end{convention}%
321 *)
322
323 alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/n.var".
324
325 alias id "m" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/m.var".
326
327 alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/P.var".
328
329 alias id "R" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/R.var".
330
331 alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/e.var".
332
333 alias id "e'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/e'.var".
334
335 alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/He.var".
336
337 alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/He'.var".
338
339 (* begin hide *)
340
341 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/d.con" "Refinement_Lemma__Third_Refinement_Lemma__".
342
343 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/d'.con" "Refinement_Lemma__Third_Refinement_Lemma__".
344
345 (* end hide *)
346
347 alias id "HMeshP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HMeshP.var".
348
349 alias id "HMeshR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HMeshR.var".
350
351 alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fP.var".
352
353 alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfP.var".
354
355 alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfP'.var".
356
357 alias id "fR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fR.var".
358
359 alias id "HfR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfR.var".
360
361 alias id "HfR'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfR'.var".
362
363 alias id "Hab'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/Hab'.var".
364
365 alias id "beta" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/beta.var".
366
367 alias id "Hbeta" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/Hbeta.var".
368
369 (* begin hide *)
370
371 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/alpha.con" "Refinement_Lemma__Third_Refinement_Lemma__".
372
373 inline "cic:/CoRN/ftc/RefLemma/RL_alpha.con".
374
375 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi1.con" "Refinement_Lemma__Third_Refinement_Lemma__".
376
377 inline "cic:/CoRN/ftc/RefLemma/RL_csi1.con".
378
379 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/delta1.con" "Refinement_Lemma__Third_Refinement_Lemma__".
380
381 inline "cic:/CoRN/ftc/RefLemma/RL_delta1.con".
382
383 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/P'.con" "Refinement_Lemma__Third_Refinement_Lemma__".
384
385 inline "cic:/CoRN/ftc/RefLemma/RL_P'_sep.con".
386
387 inline "cic:/CoRN/ftc/RefLemma/RL_P'_Mesh.con".
388
389 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fP'.con" "Refinement_Lemma__Third_Refinement_Lemma__".
390
391 inline "cic:/CoRN/ftc/RefLemma/RL_fP'_in_P'.con".
392
393 inline "cic:/CoRN/ftc/RefLemma/RL_P'_P_sum.con".
394
395 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi2.con" "Refinement_Lemma__Third_Refinement_Lemma__".
396
397 inline "cic:/CoRN/ftc/RefLemma/RL_csi2.con".
398
399 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/delta2.con" "Refinement_Lemma__Third_Refinement_Lemma__".
400
401 inline "cic:/CoRN/ftc/RefLemma/RL_delta2.con".
402
403 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/R'.con" "Refinement_Lemma__Third_Refinement_Lemma__".
404
405 inline "cic:/CoRN/ftc/RefLemma/RL_R'_sep.con".
406
407 inline "cic:/CoRN/ftc/RefLemma/RL_R'_Mesh.con".
408
409 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fR'.con" "Refinement_Lemma__Third_Refinement_Lemma__".
410
411 inline "cic:/CoRN/ftc/RefLemma/RL_fR'_in_R'.con".
412
413 inline "cic:/CoRN/ftc/RefLemma/RL_R'_R_sum.con".
414
415 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi3.con" "Refinement_Lemma__Third_Refinement_Lemma__".
416
417 inline "cic:/CoRN/ftc/RefLemma/RL_csi3.con".
418
419 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/Q.con" "Refinement_Lemma__Third_Refinement_Lemma__".
420
421 inline "cic:/CoRN/ftc/RefLemma/RL_Q_Mesh.con".
422
423 inline "cic:/CoRN/ftc/RefLemma/RL_Q_sep.con".
424
425 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fQ.con" "Refinement_Lemma__Third_Refinement_Lemma__".
426
427 inline "cic:/CoRN/ftc/RefLemma/RL_fQ_in_Q.con".
428
429 inline "cic:/CoRN/ftc/RefLemma/RL_Q_P'_sum.con".
430
431 (* end hide *)
432
433 inline "cic:/CoRN/ftc/RefLemma/third_refinement_lemma.con".
434
435 (* UNEXPORTED
436 End Third_Refinement_Lemma
437 *)
438
439 (* UNEXPORTED
440 Section Fourth_Refinement_Lemma
441 *)
442
443 (* begin hide *)
444
445 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/Fa.con" "Refinement_Lemma__Fourth_Refinement_Lemma__".
446
447 (* NOTATION
448 Notation just := (fun z => incF _ (Pts_part_lemma _ _ _ _ _ _ z _ _)).
449 *)
450
451 inline "cic:/CoRN/ftc/RefLemma/RL_sum_lemma_aux.con".
452
453 (* end hide *)
454
455 (*#*
456 Finally, this is inequality (2.6.7) exactly as stated (same conventions as
457 above)
458 *)
459
460 alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/n.var".
461
462 alias id "m" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/m.var".
463
464 alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/P.var".
465
466 alias id "R" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/R.var".
467
468 alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/e.var".
469
470 alias id "e'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/e'.var".
471
472 alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/He.var".
473
474 alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/He'.var".
475
476 (* begin hide *)
477
478 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/d.con" "Refinement_Lemma__Fourth_Refinement_Lemma__".
479
480 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/d'.con" "Refinement_Lemma__Fourth_Refinement_Lemma__".
481
482 (* end hide *)
483
484 alias id "HMeshP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HMeshP.var".
485
486 alias id "HMeshR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HMeshR.var".
487
488 alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/fP.var".
489
490 alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfP.var".
491
492 alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfP'.var".
493
494 alias id "fR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/fR.var".
495
496 alias id "HfR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfR.var".
497
498 alias id "HfR'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfR'.var".
499
500 (* begin show *)
501
502 alias id "Hab'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/Hab'.var".
503
504 (* end show *)
505
506 inline "cic:/CoRN/ftc/RefLemma/fourth_refinement_lemma.con".
507
508 (* UNEXPORTED
509 End Fourth_Refinement_Lemma
510 *)
511
512 (* UNEXPORTED
513 Section Main_Refinement_Lemma
514 *)
515
516 (*#* We finish by presenting Theorem 9. *)
517
518 alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/n.var".
519
520 alias id "m" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/m.var".
521
522 alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/P.var".
523
524 alias id "R" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/R.var".
525
526 alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/e.var".
527
528 alias id "e'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/e'.var".
529
530 alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/He.var".
531
532 alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/He'.var".
533
534 (* begin hide *)
535
536 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/d.con" "Refinement_Lemma__Main_Refinement_Lemma__".
537
538 inline "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/d'.con" "Refinement_Lemma__Main_Refinement_Lemma__".
539
540 (* end hide *)
541
542 alias id "HMeshP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HMeshP.var".
543
544 alias id "HMeshR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HMeshR.var".
545
546 alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/fP.var".
547
548 alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfP.var".
549
550 alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfP'.var".
551
552 alias id "fR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/fR.var".
553
554 alias id "HfR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfR.var".
555
556 alias id "HfR'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfR'.var".
557
558 inline "cic:/CoRN/ftc/RefLemma/refinement_lemma.con".
559
560 (* UNEXPORTED
561 End Main_Refinement_Lemma
562 *)
563
564 (* UNEXPORTED
565 End Refinement_Lemma
566 *)
567