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/reals/Intervals".
19 (* $Id: Intervals.v,v 1.10 2004/04/23 10:01:04 lcf Exp $ *)
34 In this section we define (compact) intervals of the real line and
35 some useful functions to work with them.
39 We start by defining the compact interval [[a,b]] as being the set of
40 points less or equal than [b] and greater or equal than [a]. We
41 require [a [<=] b], as we want to work only in nonempty intervals.
44 inline cic:/CoRN/reals/Intervals/compact.con.
47 %\begin{convention}% Let [a,b : IR] and [Hab : a [<=] b].
50 As expected, both [a] and [b] are members of [[a,b]]. Also they are
51 members of the interval [[Min(a,b),Max(a,b)]].
54 inline cic:/CoRN/reals/Intervals/a.var.
56 inline cic:/CoRN/reals/Intervals/b.var.
58 inline cic:/CoRN/reals/Intervals/Hab.var.
60 inline cic:/CoRN/reals/Intervals/compact_inc_lft.con.
62 inline cic:/CoRN/reals/Intervals/compact_inc_rht.con.
64 inline cic:/CoRN/reals/Intervals/compact_Min_lft.con.
66 inline cic:/CoRN/reals/Intervals/compact_Min_rht.con.
69 As we will be interested in taking functions with domain in a compact
70 interval, we want this predicate to be well defined.
73 inline cic:/CoRN/reals/Intervals/compact_wd.con.
76 Also, it will sometimes be necessary to rewrite the endpoints of an interval.
79 inline cic:/CoRN/reals/Intervals/compact_wd'.con.
82 As we identify subsets with predicates, inclusion is simply implication.
86 Finally, we define a restriction operator that takes a function [F]
87 and a well defined predicate [P] included in the domain of [F] and
88 returns the restriction $F|_P$# of F to P#.
91 inline cic:/CoRN/reals/Intervals/Frestr.con.
98 Implicit Arguments Frestr [F P].
102 Section More_Intervals.
105 inline cic:/CoRN/reals/Intervals/included_refl'.con.
107 (*#* We prove some inclusions of compact intervals. *)
109 inline cic:/CoRN/reals/Intervals/compact_map1.con.
111 inline cic:/CoRN/reals/Intervals/compact_map2.con.
113 inline cic:/CoRN/reals/Intervals/compact_map3.con.
120 Hint Resolve included_refl' compact_map1 compact_map2 compact_map3 : included.
124 Section Totally_Bounded.
127 (*#* ** Totally Bounded
129 Totally bounded sets will play an important role in what is
130 to come. The definition (equivalent to the classical one) states that
131 [P] is totally bounded iff
132 %\[\forall_{\varepsilon>0}\exists_{x_1,\ldots,x_n}\forall_{y\in P}
133 \exists_{1\leq i\leq n}|y-x_i|<\varepsilon\]%#∀e>0
134 ∃x<sub>1</sub>,...,x<sub>n</sub>∀y∈P∃
135 1≤i≤n.|y-x<sub>i</sub>|<e#.
137 Notice the use of lists for quantification.
140 inline cic:/CoRN/reals/Intervals/totally_bounded.con.
143 This definition is classically, but not constructively, equivalent to
144 the definition of compact (if completeness is assumed); the next
145 result, classically equivalent to the Heine-Borel theorem, justifies
146 that we take the definition of totally bounded to be the relevant one
147 and that we defined compacts as we did.
150 inline cic:/CoRN/reals/Intervals/compact_is_totally_bounded.con.
153 Suprema and infima will be needed throughout; we define them here both
154 for arbitrary subsets of [IR] and for images of functions.
157 inline cic:/CoRN/reals/Intervals/set_glb_IR.con.
159 inline cic:/CoRN/reals/Intervals/set_lub_IR.con.
161 inline cic:/CoRN/reals/Intervals/fun_image.con.
163 inline cic:/CoRN/reals/Intervals/fun_glb_IR.con.
165 inline cic:/CoRN/reals/Intervals/fun_lub_IR.con.
169 inline cic:/CoRN/reals/Intervals/aux_seq_lub.con.
171 inline cic:/CoRN/reals/Intervals/aux_seq_lub_prop.con.
176 The following are probably the most important results in this section.
179 inline cic:/CoRN/reals/Intervals/totally_bounded_has_lub.con.
183 inline cic:/CoRN/reals/Intervals/aux_seq_glb.con.
185 inline cic:/CoRN/reals/Intervals/aux_seq_glb_prop.con.
189 inline cic:/CoRN/reals/Intervals/totally_bounded_has_glb.con.
201 In this section we dwell a bit farther into the definition of compactness
202 and explore some of its properties.
204 The following characterization of inclusion can be very useful:
207 inline cic:/CoRN/reals/Intervals/included_compact.con.
210 At several points in our future development of a theory we will need
211 to partition a compact interval in subintervals of length smaller than
212 some predefined value [eps]. Although this seems a
213 consequence of every compact interval being totally bounded, it is in
214 fact a stronger property. In this section we perform that
215 construction (requiring the endpoints of the interval to be distinct)
216 and prove some of its good properties.
218 %\begin{convention}% Let [a,b : IR], [Hab : (a [<=] b)] and denote by [I]
219 the compact interval [[a,b]]. Also assume that [a [<] b], and let [e] be
220 a positive real number.
224 inline cic:/CoRN/reals/Intervals/a.var.
226 inline cic:/CoRN/reals/Intervals/b.var.
228 inline cic:/CoRN/reals/Intervals/Hab.var.
232 inline cic:/CoRN/reals/Intervals/I.con.
236 inline cic:/CoRN/reals/Intervals/Hab'.var.
238 inline cic:/CoRN/reals/Intervals/e.var.
240 inline cic:/CoRN/reals/Intervals/He.var.
243 We start by finding a natural number [n] such that [(b[-]a) [/] n [<] e].
246 inline cic:/CoRN/reals/Intervals/compact_nat.con.
248 (*#* Obviously such an [n] must be greater than zero.*)
250 inline cic:/CoRN/reals/Intervals/pos_compact_nat.con.
253 We now define a sequence on [n] points in [[a,b]] by
254 [x_i [=] Min(a,b) [+]i[*] (b[-]a) [/]n] and
255 prove that all of its points are really in that interval.
258 inline cic:/CoRN/reals/Intervals/compact_part.con.
260 inline cic:/CoRN/reals/Intervals/compact_part_hyp.con.
263 This sequence is strictly increasing and each two consecutive points
264 are apart by less than [e].*)
266 inline cic:/CoRN/reals/Intervals/compact_less.con.
268 inline cic:/CoRN/reals/Intervals/compact_leEq.con.
270 (*#* When we proceed to integration, this lemma will also be useful: *)
272 inline cic:/CoRN/reals/Intervals/compact_partition_lemma.con.
274 (*#* The next lemma provides an upper bound for the distance between two points in an interval: *)
276 inline cic:/CoRN/reals/Intervals/compact_elements.con.
282 (*#* The following is a variation on the previous lemma: *)
284 inline cic:/CoRN/reals/Intervals/compact_elements'.con.
286 (*#* The following lemma is a bit more specific: it shows that we can
287 also estimate the distance from the center of a compact interval to
288 any of its points. *)
290 inline cic:/CoRN/reals/Intervals/compact_bnd_AbsIR.con.
292 (*#* Finally, two more useful lemmas to prove inclusion of compact
293 intervals. They will be necessary for the definition and proof of the
294 elementary properties of the integral. *)
296 inline cic:/CoRN/reals/Intervals/included2_compact.con.
298 inline cic:/CoRN/reals/Intervals/included3_compact.con.
305 Hint Resolve included_compact included2_compact included3_compact : included.