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 *********************)
19 (* $Id: RefLemma.v,v 1.7 2004/04/23 10:01:00 lcf Exp $ *)
21 include "ftc/RefSeparating.ma".
23 include "ftc/RefSeparated.ma".
25 include "ftc/RefSepRef.ma".
28 Section Refinement_Lemma
31 (*#* *The Refinement Lemmas
33 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):
35 %\noindent\textbf{%#<b>#Theorem#</b>#%}% Let [f] be a continuous function on a
36 compact interval [[a,b]] with modulus of continuity%\footnote{%# (#From our
37 point of view, the modulus of continuity is simply the proof that [f] is
38 continuous.#)#%}% [omega].
39 Let [P] be a partition of [[a,b]] and [eps [>] Zero] be such that
40 [mesh(P) [<] omega(eps)].
42 %\[\left|S(f,P)-\int_a^bf(x)dx\right|\leq\varepsilon(b-a),\]%#|S(f,P)-∫f(x)dx|≤ε(b-a)#
43 where [S(f,P)] denotes any sum of the function [f] respecting the partition
44 [P] (as previously defined).
46 The proof of this theorem relies on the fact that for any two partitions [P]
47 and [R] of [[a,b]] it is possible to define a partition [Q] which is
48 ``almost'' a common refinement of [P] and [R]---that is, given [eps [>] Zero]
49 it is possible to define [Q] such that for every point [x] of either [P] or
50 [R] there is a point [y] of [Q] such that [|x[-]y| [<] eps].
51 This requires three separate constructions (done in three separate files)
52 which are then properly combined to give the final result. We recommend the
53 reader to ignore this technical constructions.
55 First we prove that if [P] and [R] are both
56 separated (though not necessarily separated from each other) then we can
57 define a partition [P'] arbitrarily close to [P] (that is, such that given
58 [alpha [>] Zero] and [xi [>] Zero] [P'] satisfies both
59 [mesh(P') [<] mesh(P) [+] xi] and for every choice of points [x_i] respecting
60 [P] there is a choice of points [x'_i] respecting [P'] such that
61 [|S(f,P)-S(f,P')| [<] alpha]) that is separated from [R].
63 Then we prove that given any partition [P]
64 and assuming [a [#] b] we can define a partition [P'] arbitrarily close to
65 [P] (in the same sense as above) which is separated.
67 Finally we prove that every two separated
68 partitions [P] and [R] have a common refinement---as every two points in [P]
69 and [R] are apart, we can decide which one is smaller. We use here the
70 technical results about ordering that we proved in the file [IntegralLemmas.v].
72 Using the results from these files, we prove our main lemma in several steps
75 %\begin{convention}% Throughout this section:
76 - [a,b:IR] and [I] denotes [[a,b]];
77 - [F] is a partial function continuous in [I].
82 alias id "a" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/a.var".
84 alias id "b" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/b.var".
86 alias id "Hab" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Hab.var".
90 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/I.con" "Refinement_Lemma__" as definition.
94 alias id "F" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/F.var".
96 alias id "contF" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/contF.var".
98 alias id "incF" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/incF.var".
102 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/contF'.con" "Refinement_Lemma__" as definition.
107 Section First_Refinement_Lemma
111 This is the first part of the proof of Theorem 2.9.
114 - [P, Q] are partitions of [I] with, respectively, [n] and [m] points;
115 - [Q] is a refinement of [P];
116 - [e] is a positive real number;
117 - [d] is the modulus of continuity of [F] for [e];
118 - the mesh of [P] is less or equal to [d];
119 - [fP] and [fQ] are choices of points respecting the partitions [P] and [Q],
125 alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/e.var".
127 alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/He.var".
131 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/d.con" "Refinement_Lemma__First_Refinement_Lemma__" as definition.
135 alias id "m" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/m.var".
137 alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/n.var".
139 alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/P.var".
141 alias id "HMesh" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HMesh.var".
143 alias id "Q" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/Q.var".
145 alias id "Href" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/Href.var".
147 alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/fP.var".
149 alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfP.var".
151 alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfP'.var".
153 alias id "fQ" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/fQ.var".
155 alias id "HfQ" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfQ.var".
157 alias id "HfQ'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/HfQ'.var".
161 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/sub.con" "Refinement_Lemma__First_Refinement_Lemma__" as definition.
163 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_0.con" as lemma.
165 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_n.con" as lemma.
167 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_mon.con" as lemma.
169 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_mon'.con" as lemma.
171 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_hyp.con" as lemma.
173 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_S.con" as lemma.
175 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H.con" "Refinement_Lemma__First_Refinement_Lemma__" as definition.
177 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H'.con" "Refinement_Lemma__First_Refinement_Lemma__" as definition.
179 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/First_Refinement_Lemma/H0.con" "Refinement_Lemma__First_Refinement_Lemma__" as definition.
181 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sub_SS.con" as lemma.
183 inline procedural "cic:/CoRN/ftc/RefLemma/RL_h.con" as definition.
185 inline procedural "cic:/CoRN/ftc/RefLemma/RL_g.con" as definition.
195 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc1.con" as lemma.
198 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfP _ _)).
202 Notation just2 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfQ _ _)).
205 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc2.con" as lemma.
207 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc3.con" as lemma.
209 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc4.con" as lemma.
211 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc5.con" as lemma.
213 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc6.con" as lemma.
215 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc7.con" as lemma.
217 inline procedural "cic:/CoRN/ftc/RefLemma/ref_calc8.con" as lemma.
221 inline procedural "cic:/CoRN/ftc/RefLemma/first_refinement_lemma.con" as lemma.
224 End First_Refinement_Lemma
228 Section Second_Refinement_Lemma
232 This is inequality (2.6.7).
235 - [P, Q, R] are partitions of [I] with, respectively, [j, n] and [k] points;
236 - [Q] is a common refinement of [P] and [R];
237 - [e, e'] are positive real numbers;
238 - [d, d'] are the moduli of continuity of [F] for [e, e'];
239 - the Mesh of [P] is less or equal to [d];
240 - the Mesh of [R] is less or equal to [d'];
241 - [fP, fQ] and [fR] are choices of points respecting the partitions [P, Q]
242 and [R], respectively.
247 alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/n.var".
249 alias id "j" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/j.var".
251 alias id "k" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/k.var".
253 alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/P.var".
255 alias id "Q" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/Q.var".
257 alias id "R" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/R.var".
259 alias id "HrefP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HrefP.var".
261 alias id "HrefR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HrefR.var".
263 alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/e.var".
265 alias id "e'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/e'.var".
267 alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/He.var".
269 alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/He'.var".
273 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/d.con" "Refinement_Lemma__Second_Refinement_Lemma__" as definition.
275 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/d'.con" "Refinement_Lemma__Second_Refinement_Lemma__" as definition.
279 alias id "HMeshP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HMeshP.var".
281 alias id "HMeshR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HMeshR.var".
283 alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/fP.var".
285 alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfP.var".
287 alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfP'.var".
289 alias id "fR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/fR.var".
291 alias id "HfR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfR.var".
293 alias id "HfR'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Second_Refinement_Lemma/HfR'.var".
295 inline procedural "cic:/CoRN/ftc/RefLemma/second_refinement_lemma.con" as lemma.
298 End Second_Refinement_Lemma
302 Section Third_Refinement_Lemma
306 This is an approximation of inequality (2.6.7), but without assuming the existence of a common refinement of [P] and [R].
309 - [P, R] are partitions of [I] with, respectively, [n] and [m] points;
310 - [e, e'] are positive real numbers;
311 - [d, d'] are the moduli of continuity of [F] for [e, e'];
312 - the Mesh of [P] is less than [d];
313 - the Mesh of [R] is less than [d'];
314 - [fP] and [fR] are choices of points respecting the partitions [P] and [R],
316 - [beta] is a positive real number.
321 alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/n.var".
323 alias id "m" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/m.var".
325 alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/P.var".
327 alias id "R" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/R.var".
329 alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/e.var".
331 alias id "e'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/e'.var".
333 alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/He.var".
335 alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/He'.var".
339 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/d.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
341 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/d'.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
345 alias id "HMeshP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HMeshP.var".
347 alias id "HMeshR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HMeshR.var".
349 alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fP.var".
351 alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfP.var".
353 alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfP'.var".
355 alias id "fR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fR.var".
357 alias id "HfR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfR.var".
359 alias id "HfR'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/HfR'.var".
361 alias id "Hab'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/Hab'.var".
363 alias id "beta" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/beta.var".
365 alias id "Hbeta" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/Hbeta.var".
369 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/alpha.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
371 inline procedural "cic:/CoRN/ftc/RefLemma/RL_alpha.con" as lemma.
373 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi1.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
375 inline procedural "cic:/CoRN/ftc/RefLemma/RL_csi1.con" as lemma.
377 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/delta1.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
379 inline procedural "cic:/CoRN/ftc/RefLemma/RL_delta1.con" as lemma.
381 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/P'.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
383 inline procedural "cic:/CoRN/ftc/RefLemma/RL_P'_sep.con" as lemma.
385 inline procedural "cic:/CoRN/ftc/RefLemma/RL_P'_Mesh.con" as lemma.
387 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fP'.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
389 inline procedural "cic:/CoRN/ftc/RefLemma/RL_fP'_in_P'.con" as lemma.
391 inline procedural "cic:/CoRN/ftc/RefLemma/RL_P'_P_sum.con" as lemma.
393 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi2.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
395 inline procedural "cic:/CoRN/ftc/RefLemma/RL_csi2.con" as lemma.
397 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/delta2.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
399 inline procedural "cic:/CoRN/ftc/RefLemma/RL_delta2.con" as lemma.
401 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/R'.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
403 inline procedural "cic:/CoRN/ftc/RefLemma/RL_R'_sep.con" as lemma.
405 inline procedural "cic:/CoRN/ftc/RefLemma/RL_R'_Mesh.con" as lemma.
407 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fR'.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
409 inline procedural "cic:/CoRN/ftc/RefLemma/RL_fR'_in_R'.con" as lemma.
411 inline procedural "cic:/CoRN/ftc/RefLemma/RL_R'_R_sum.con" as lemma.
413 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/csi3.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
415 inline procedural "cic:/CoRN/ftc/RefLemma/RL_csi3.con" as lemma.
417 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/Q.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
419 inline procedural "cic:/CoRN/ftc/RefLemma/RL_Q_Mesh.con" as lemma.
421 inline procedural "cic:/CoRN/ftc/RefLemma/RL_Q_sep.con" as lemma.
423 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Third_Refinement_Lemma/fQ.con" "Refinement_Lemma__Third_Refinement_Lemma__" as definition.
425 inline procedural "cic:/CoRN/ftc/RefLemma/RL_fQ_in_Q.con" as lemma.
427 inline procedural "cic:/CoRN/ftc/RefLemma/RL_Q_P'_sum.con" as lemma.
431 inline procedural "cic:/CoRN/ftc/RefLemma/third_refinement_lemma.con" as lemma.
434 End Third_Refinement_Lemma
438 Section Fourth_Refinement_Lemma
443 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/Fa.con" "Refinement_Lemma__Fourth_Refinement_Lemma__" as definition.
446 Notation just := (fun z => incF _ (Pts_part_lemma _ _ _ _ _ _ z _ _)).
449 inline procedural "cic:/CoRN/ftc/RefLemma/RL_sum_lemma_aux.con" as lemma.
454 Finally, this is inequality (2.6.7) exactly as stated (same conventions as
458 alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/n.var".
460 alias id "m" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/m.var".
462 alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/P.var".
464 alias id "R" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/R.var".
466 alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/e.var".
468 alias id "e'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/e'.var".
470 alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/He.var".
472 alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/He'.var".
476 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/d.con" "Refinement_Lemma__Fourth_Refinement_Lemma__" as definition.
478 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/d'.con" "Refinement_Lemma__Fourth_Refinement_Lemma__" as definition.
482 alias id "HMeshP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HMeshP.var".
484 alias id "HMeshR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HMeshR.var".
486 alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/fP.var".
488 alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfP.var".
490 alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfP'.var".
492 alias id "fR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/fR.var".
494 alias id "HfR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfR.var".
496 alias id "HfR'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/HfR'.var".
500 alias id "Hab'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Fourth_Refinement_Lemma/Hab'.var".
504 inline procedural "cic:/CoRN/ftc/RefLemma/fourth_refinement_lemma.con" as lemma.
507 End Fourth_Refinement_Lemma
511 Section Main_Refinement_Lemma
514 (*#* We finish by presenting Theorem 9. *)
516 alias id "n" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/n.var".
518 alias id "m" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/m.var".
520 alias id "P" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/P.var".
522 alias id "R" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/R.var".
524 alias id "e" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/e.var".
526 alias id "e'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/e'.var".
528 alias id "He" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/He.var".
530 alias id "He'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/He'.var".
534 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/d.con" "Refinement_Lemma__Main_Refinement_Lemma__" as definition.
536 inline procedural "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/d'.con" "Refinement_Lemma__Main_Refinement_Lemma__" as definition.
540 alias id "HMeshP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HMeshP.var".
542 alias id "HMeshR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HMeshR.var".
544 alias id "fP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/fP.var".
546 alias id "HfP" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfP.var".
548 alias id "HfP'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfP'.var".
550 alias id "fR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/fR.var".
552 alias id "HfR" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfR.var".
554 alias id "HfR'" = "cic:/CoRN/ftc/RefLemma/Refinement_Lemma/Main_Refinement_Lemma/HfR'.var".
556 inline procedural "cic:/CoRN/ftc/RefLemma/refinement_lemma.con" as lemma.
559 End Main_Refinement_Lemma