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: MoreIntervals.v,v 1.6 2004/04/23 10:00:59 lcf Exp $ *)
21 include "ftc/NthDerivative.ma".
31 (*#* printing realline %\ensuremath{\RR}% #(-∞,+∞)# *)
33 (*#* printing openl %\ensuremath{(\cdot,+\infty)}% #(⋅,+∞)# *)
35 (*#* printing openr %\ensuremath{(-\infty,\cdot)}% #(-∞,⋅)# *)
37 (*#* printing closel %\ensuremath{[\cdot,+\infty)}% #[⋅,+∞)# *)
39 (*#* printing closer %\ensuremath{(-\infty,\cdot]}% #(-∞,⋅]# *)
41 (*#* printing olor %\ensuremath{(\cdot,\cdot)}% #(⋅,⋅)# *)
43 (*#* printing clor %\ensuremath{[\cdot,\cdot)}% #[⋅,⋅)# *)
45 (*#* printing olcr %\ensuremath{(\cdot,\cdot]}% #(⋅,⋅]# *)
47 (*#* printing clcr %\ensuremath{[\cdot,\cdot]}% #[⋅,⋅]# *)
49 (*#* *Generalized Intervals
51 At this stage we have enough material to begin generalizing our
52 concepts in preparation for the fundamental theorem of calculus and
53 the definition of the main (non-polynomial) functions of analysis.
55 In order to define functions via power series (or any other kind of
56 series) we need to formalize a notion of convergence more general than
57 the one we already have on compact intervals. This is necessary for
58 practical reasons: we want to define a single exponential function
59 with domain [IR], not several exponential functions defined on compact
60 intervals which we prove to be the same wherever their domains
61 overlap. In a similar way, we want to define indefinite integrals on
62 infinite domains and not only on compact intervals.
64 Unfortunately, proceeding in a way analogous to how we defined the
65 concept of global continuity will lead us nowhere; the concept turns
66 out to be to general, and the behaviour on too small domains
67 (typically intervals [[a,a']] where [a [=] a'] is neither
68 provably true nor provably false) will be unsatisfactory.
70 There is a special family of sets, however, where this problems can be
71 avoided: intervals. Intervals have some nice properties that allow us
72 to prove good results, namely the facts that if [a] and [b] are
73 elements of an interval [I] then so are [Min(a,b)] and
74 [Max(a,b)] (which is in general not true) and also the
75 compact interval [[a,b]] is included in [I]. Furthermore, all
76 intervals are characterized by simple, well defined predicates, and
77 the nonempty and proper concepts become very easy to define.
79 **Definitions and Basic Results
81 We define an inductive type of intervals with nine constructors,
82 corresponding to the nine basic types of intervals. The reason why so
83 many constructors are needed is that we do not have a notion of real
84 line, for many reasons which we will not discuss here. Also it seems
85 simple to directly define finite intervals than to define then later
86 as intersections of infinite intervals, as it would only mess things
89 The compact interval which we will define here is obviously the same
90 that we have been working with all the way through; why, then, the
91 different formulation? The reason is simple: if we had worked with
92 intervals from the beginning we would have had case definitions at
93 every spot, and our lemmas and proofs would have been very awkward.
94 Also, it seems more natural to characterize a compact interval by two
95 real numbers (and a proof) than as a particular case of a more general
96 concept which doesn't have an intuitive interpretation. Finally, the
97 definitions we will make here will have the elegant consequence that
98 from this point on we can work with any kind of intervals in exactly
102 inline procedural "cic:/CoRN/ftc/MoreIntervals/interval.ind".
105 To each interval a predicate (set) is assigned by the following map:
108 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop.con" as definition.
113 cic:/matita/CoRN-Procedural/ftc/MoreIntervals/iprop.con
119 This map is made into a coercion, so that intervals
120 %\emph{%#<i>#are%}%#</i># really subsets of reals.
122 We now define what it means for an interval to be nonvoid, proper,
123 finite and compact in the obvious way.
126 inline procedural "cic:/CoRN/ftc/MoreIntervals/nonvoid.con" as definition.
128 inline procedural "cic:/CoRN/ftc/MoreIntervals/proper.con" as definition.
130 inline procedural "cic:/CoRN/ftc/MoreIntervals/finite.con" as definition.
132 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_.con" as definition.
134 (*#* Finite intervals have a left end and a right end. *)
136 inline procedural "cic:/CoRN/ftc/MoreIntervals/left_end.con" as definition.
138 inline procedural "cic:/CoRN/ftc/MoreIntervals/right_end.con" as definition.
141 Some trivia: compact intervals are finite; proper intervals are nonvoid; an interval is nonvoid iff it contains some point.
144 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_finite.con" as lemma.
146 inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_nonvoid.con" as lemma.
148 inline procedural "cic:/CoRN/ftc/MoreIntervals/nonvoid_point.con" as lemma.
150 inline procedural "cic:/CoRN/ftc/MoreIntervals/nonvoid_char.con" as lemma.
153 For practical reasons it helps to define left end and right end of compact intervals.
156 inline procedural "cic:/CoRN/ftc/MoreIntervals/Lend.con" as definition.
158 inline procedural "cic:/CoRN/ftc/MoreIntervals/Rend.con" as definition.
160 (*#* In a compact interval, the left end is always less than or equal
164 inline procedural "cic:/CoRN/ftc/MoreIntervals/Lend_leEq_Rend.con" as lemma.
167 Some nice characterizations of inclusion:
170 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_included.con" as lemma.
172 inline procedural "cic:/CoRN/ftc/MoreIntervals/included_interval'.con" as lemma.
174 inline procedural "cic:/CoRN/ftc/MoreIntervals/included_interval.con" as lemma.
177 A weirder inclusion result.
180 inline procedural "cic:/CoRN/ftc/MoreIntervals/included3_interval.con" as lemma.
183 Finally, all intervals are characterized by well defined predicates.
186 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_wd.con" as lemma.
193 Implicit Arguments Lend [I].
197 Implicit Arguments Rend [I].
201 Section Compact_Constructions
205 Section Single_Compact_Interval
208 (*#* **Constructions with Compact Intervals
210 Several important constructions are now discussed.
212 We begin by defining the compact interval [[x,x]].
214 %\begin{convention}% Let [P:IR->CProp] be well defined, and [x:IR]
215 such that [P(x)] holds.
220 cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/P.var
224 cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/wdP.var
228 cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/x.var
232 cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/Hx.var
235 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_single.con" as definition.
238 This interval contains [x] and only (elements equal to) [x]; furthermore, for every (well-defined) [P], if $x\in P$#x∈P# then $[x,x]\subseteq P$#[x,x]⊆P#.
241 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_single_prop.con" as lemma.
243 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_single_pt.con" as lemma.
245 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_single_inc.con" as lemma.
248 End Single_Compact_Interval
252 The special case of intervals is worth singling out, as one of the hypothesis becomes a theorem.
255 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_single_iprop.con" as definition.
258 Now for more interesting and important results.
260 Let [I] be a proper interval and [x] be a point of [I]. Then there is
261 a proper compact interval [[a,b]] such that $x\in[a,b]\subseteq
262 I$#x∈[a,b]⊆I#.
266 Section Proper_Compact_with_One_or_Two_Points
271 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1'.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
273 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
275 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1'''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
277 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1''''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
279 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
281 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2'.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
283 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
285 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2'''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
287 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
289 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3'.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
291 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
293 inline procedural "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3'''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__" as definition.
297 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval.con" as definition.
299 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_compact_in_interval.con" as lemma.
301 inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval.con" as lemma.
303 inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval'.con" as lemma.
305 inline procedural "cic:/CoRN/ftc/MoreIntervals/included_compact_in_interval.con" as lemma.
307 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval.con" as lemma.
309 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval'.con" as lemma.
311 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval_inc1.con" as lemma.
313 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval_inc2.con" as lemma.
316 If [x [=] y] then the construction yields the same interval whether we
317 use [x] or [y] in its definition. This property is required at some
318 stage, which is why we formalized this result as a functional
319 definition rather than as an existential formula.
322 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_wd1.con" as lemma.
324 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_wd2.con" as lemma.
327 We can make an analogous construction for two points.
330 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval2.con" as definition.
332 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_compact_in_interval2.con" as lemma.
334 inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval2.con" as lemma.
336 inline procedural "cic:/CoRN/ftc/MoreIntervals/proper_compact_in_interval2'.con" as lemma.
338 inline procedural "cic:/CoRN/ftc/MoreIntervals/included_compact_in_interval2.con" as lemma.
340 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2x.con" as lemma.
342 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2y.con" as lemma.
344 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2x'.con" as lemma.
346 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2y'.con" as lemma.
348 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2_inc1.con" as lemma.
350 inline procedural "cic:/CoRN/ftc/MoreIntervals/iprop_compact_in_interval2_inc2.con" as lemma.
352 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_x_lft.con" as lemma.
354 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_y_lft.con" as lemma.
356 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_x_rht.con" as lemma.
358 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_y_rht.con" as lemma.
361 End Proper_Compact_with_One_or_Two_Points
365 Compact intervals are exactly compact intervals(!).
368 inline procedural "cic:/CoRN/ftc/MoreIntervals/interval_compact_inc.con" as lemma.
370 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_interval_inc.con" as lemma.
373 A generalization of the previous results: if $[a,b]\subseteq J$#[a,b]⊆J#
374 and [J] is proper, then we can find a proper interval [[a',b']] such that
375 $[a,b]\subseteq[a',b']\subseteq J$#[a,b]⊆[a',b']⊆J#.
378 inline procedural "cic:/CoRN/ftc/MoreIntervals/compact_proper_in_interval.con" as lemma.
381 End Compact_Constructions
388 (*#* **Properties of Functions in Intervals
390 We now define notions of continuity, differentiability and so on on
391 arbitrary intervals. As expected, a function [F] has property [P] in
392 the (proper) interval [I] iff it has property [P] in every compact
393 interval included in [I]. We can formalize this in a nice way using
394 previously defined concepts.
396 %\begin{convention}% Let [n:nat] and [I:interval].
401 cic:/CoRN/ftc/MoreIntervals/Functions/n.var
405 cic:/CoRN/ftc/MoreIntervals/Functions/I.var
408 inline procedural "cic:/CoRN/ftc/MoreIntervals/Continuous.con" as definition.
410 inline procedural "cic:/CoRN/ftc/MoreIntervals/Derivative.con" as definition.
412 inline procedural "cic:/CoRN/ftc/MoreIntervals/Diffble.con" as definition.
414 inline procedural "cic:/CoRN/ftc/MoreIntervals/Derivative_n.con" as definition.
416 inline procedural "cic:/CoRN/ftc/MoreIntervals/Diffble_n.con" as definition.
423 Section Reflexivity_Properties
427 In the case of compact intervals, this definitions collapse to the old ones.
430 inline procedural "cic:/CoRN/ftc/MoreIntervals/Continuous_Int.con" as lemma.
432 inline procedural "cic:/CoRN/ftc/MoreIntervals/Int_Continuous.con" as lemma.
434 inline procedural "cic:/CoRN/ftc/MoreIntervals/Derivative_Int.con" as lemma.
436 inline procedural "cic:/CoRN/ftc/MoreIntervals/Int_Derivative.con" as lemma.
438 inline procedural "cic:/CoRN/ftc/MoreIntervals/Diffble_Int.con" as lemma.
440 inline procedural "cic:/CoRN/ftc/MoreIntervals/Int_Diffble.con" as lemma.
443 End Reflexivity_Properties
451 Interestingly, inclusion and equality in an interval are also characterizable in a similar way:
454 inline procedural "cic:/CoRN/ftc/MoreIntervals/included_imp_inc.con" as lemma.
456 inline procedural "cic:/CoRN/ftc/MoreIntervals/included_Feq''.con" as lemma.
458 inline procedural "cic:/CoRN/ftc/MoreIntervals/included_Feq'.con" as lemma.
465 Hint Resolve included_interval included_interval' included3_interval
466 compact_single_inc compact_single_iprop included_compact_in_interval
467 iprop_compact_in_interval_inc1 iprop_compact_in_interval_inc2
468 included_compact_in_interval2 iprop_compact_in_interval2_inc1
469 iprop_compact_in_interval2_inc2 interval_compact_inc compact_interval_inc