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/Continuity".
19 (* $Id: Continuity.v,v 1.6 2004/04/23 10:00:58 lcf Exp $ *)
21 (*#* printing Norm_Funct %\ensuremath{\|\cdot\|}% *)
32 Section Definitions_and_Basic_Results.
37 Constructively, continuity is the most fundamental property of any
38 function---so strongly that no example is known of a constructive
39 function that is not continuous. However, the classical definition of
40 continuity is not good for our purposes, as it is not true, for
41 example, that a function which is continuous in a compact interval is
42 uniformly continuous in that same interval (for a discussion of this
43 see Bishop 1967). Thus, our notion of continuity will be the uniform
44 one#. #%\footnote{%Similar remarks apply to convergence of sequences
45 of functions, which we will define ahead, and elsewhere; we will
46 refrain from discussing this issue at those places.%}.%
48 %\begin{convention}% Throughout this section, [a] and [b] will be real
49 numbers, [I] will denote the compact interval [[a,b]] and
50 [F, G, H] will denote arbitrary partial functions with domains
51 respectively [P, Q] and [R].
54 ** Definitions and Basic Results
56 Here we define continuity and prove some basic properties of continuous functions.
59 inline cic:/CoRN/ftc/Continuity/a.var.
61 inline cic:/CoRN/ftc/Continuity/b.var.
63 inline cic:/CoRN/ftc/Continuity/Hab.var.
67 inline cic:/CoRN/ftc/Continuity/I.con.
71 inline cic:/CoRN/ftc/Continuity/F.var.
75 inline cic:/CoRN/ftc/Continuity/P.con.
79 inline cic:/CoRN/ftc/Continuity/Continuous_I.con.
82 For convenience, we distinguish the two properties of continuous functions.
85 inline cic:/CoRN/ftc/Continuity/contin_imp_inc.con.
87 inline cic:/CoRN/ftc/Continuity/contin_prop.con.
90 Assume [F] to be continuous in [I]. Then it has a least upper bound and a greater lower bound on [I].
93 inline cic:/CoRN/ftc/Continuity/contF.var.
97 inline cic:/CoRN/ftc/Continuity/Hinc'.con.
101 inline cic:/CoRN/ftc/Continuity/Continuous_I_imp_tb_image.con.
103 inline cic:/CoRN/ftc/Continuity/Continuous_I_imp_lub.con.
105 inline cic:/CoRN/ftc/Continuity/Continuous_I_imp_glb.con.
108 We now make this glb and lub into operators.
111 inline cic:/CoRN/ftc/Continuity/lub_funct.con.
113 inline cic:/CoRN/ftc/Continuity/glb_funct.con.
116 These operators have the expected properties.
119 inline cic:/CoRN/ftc/Continuity/lub_is_lub.con.
121 inline cic:/CoRN/ftc/Continuity/glb_is_glb.con.
123 inline cic:/CoRN/ftc/Continuity/glb_prop.con.
125 inline cic:/CoRN/ftc/Continuity/lub_prop.con.
128 The norm of a function is defined as being the supremum of its absolute value; that is equivalent to the following definition (which is often more convenient to use).
131 inline cic:/CoRN/ftc/Continuity/Norm_Funct.con.
134 The norm effectively bounds the absolute value of a function.
137 inline cic:/CoRN/ftc/Continuity/norm_bnd_AbsIR.con.
140 The following is another way of characterizing the norm:
143 inline cic:/CoRN/ftc/Continuity/Continuous_I_imp_abs_lub.con.
146 We now prove some basic properties of the norm---namely that it is positive, and that it provides a least upper bound for the absolute value of its argument.
149 inline cic:/CoRN/ftc/Continuity/positive_norm.con.
151 inline cic:/CoRN/ftc/Continuity/norm_fun_lub.con.
153 inline cic:/CoRN/ftc/Continuity/leEq_Norm_Funct.con.
155 inline cic:/CoRN/ftc/Continuity/less_Norm_Funct.con.
158 End Definitions_and_Basic_Results.
162 Implicit Arguments Continuous_I [a b].
166 Implicit Arguments Norm_Funct [a b Hab F].
170 Section Local_Results.
173 (*#* **Algebraic Properties
175 We now state and prove some results about continuous functions. Assume that [I] is included in the domain of both [F] and [G].
178 inline cic:/CoRN/ftc/Continuity/a.var.
180 inline cic:/CoRN/ftc/Continuity/b.var.
182 inline cic:/CoRN/ftc/Continuity/Hab.var.
186 inline cic:/CoRN/ftc/Continuity/I.con.
190 inline cic:/CoRN/ftc/Continuity/F.var.
192 inline cic:/CoRN/ftc/Continuity/G.var.
196 inline cic:/CoRN/ftc/Continuity/P.con.
198 inline cic:/CoRN/ftc/Continuity/Q.con.
202 inline cic:/CoRN/ftc/Continuity/incF.var.
204 inline cic:/CoRN/ftc/Continuity/incG.var.
207 The first result does not require the function to be continuous; however, its preconditions are easily verified by continuous functions, which justifies its inclusion in this section.
210 inline cic:/CoRN/ftc/Continuity/cont_no_sign_change.con.
212 inline cic:/CoRN/ftc/Continuity/cont_no_sign_change_pos.con.
214 inline cic:/CoRN/ftc/Continuity/cont_no_sign_change_neg.con.
217 Being continuous is an extensional property.
220 inline cic:/CoRN/ftc/Continuity/Continuous_I_wd.con.
223 A continuous function remains continuous if you restrict its domain.
226 inline cic:/CoRN/ftc/Continuity/included_imp_contin.con.
229 Constant functions and identity are continuous.
232 inline cic:/CoRN/ftc/Continuity/Continuous_I_const.con.
234 inline cic:/CoRN/ftc/Continuity/Continuous_I_id.con.
237 Assume [F] and [G] are continuous in [I]. Then functions derived from these through algebraic operations are also continuous, provided (in the case of reciprocal and division) some extra conditions are met.
240 inline cic:/CoRN/ftc/Continuity/contF.var.
242 inline cic:/CoRN/ftc/Continuity/contG.var.
244 inline cic:/CoRN/ftc/Continuity/Continuous_I_plus.con.
246 inline cic:/CoRN/ftc/Continuity/Continuous_I_inv.con.
248 inline cic:/CoRN/ftc/Continuity/Continuous_I_mult.con.
255 Transparent AbsIR Max.
258 inline cic:/CoRN/ftc/Continuity/Continuous_I_max.con.
262 inline cic:/CoRN/ftc/Continuity/Hg'.var.
264 inline cic:/CoRN/ftc/Continuity/Hg''.var.
268 inline cic:/CoRN/ftc/Continuity/Continuous_I_recip.con.
275 Hint Resolve contin_imp_inc: included.
282 inline cic:/CoRN/ftc/Continuity/a.var.
284 inline cic:/CoRN/ftc/Continuity/b.var.
286 inline cic:/CoRN/ftc/Continuity/Hab.var.
290 inline cic:/CoRN/ftc/Continuity/I.con.
294 inline cic:/CoRN/ftc/Continuity/F.var.
296 inline cic:/CoRN/ftc/Continuity/G.var.
300 inline cic:/CoRN/ftc/Continuity/P.con.
302 inline cic:/CoRN/ftc/Continuity/Q.con.
306 inline cic:/CoRN/ftc/Continuity/contF.var.
308 inline cic:/CoRN/ftc/Continuity/contG.var.
311 The corresponding properties for subtraction, division and
312 multiplication by a scalar are easily proved as corollaries;
313 exponentiation is proved by induction, appealing to the results on
314 product and constant functions.
317 inline cic:/CoRN/ftc/Continuity/Continuous_I_minus.con.
319 inline cic:/CoRN/ftc/Continuity/Continuous_I_scal.con.
321 inline cic:/CoRN/ftc/Continuity/Continuous_I_nth.con.
323 inline cic:/CoRN/ftc/Continuity/Continuous_I_min.con.
325 inline cic:/CoRN/ftc/Continuity/Continuous_I_abs.con.
327 inline cic:/CoRN/ftc/Continuity/Hg'.var.
329 inline cic:/CoRN/ftc/Continuity/Hg''.var.
331 inline cic:/CoRN/ftc/Continuity/Continuous_I_div.con.
346 We finally prove that the sum of an arbitrary family of continuous functions is still a continuous function.
349 inline cic:/CoRN/ftc/Continuity/a.var.
351 inline cic:/CoRN/ftc/Continuity/b.var.
353 inline cic:/CoRN/ftc/Continuity/Hab.var.
355 inline cic:/CoRN/ftc/Continuity/Hab'.var.
359 inline cic:/CoRN/ftc/Continuity/I.con.
363 inline cic:/CoRN/ftc/Continuity/Continuous_I_Sum0.con.
365 inline cic:/CoRN/ftc/Continuity/Continuous_I_Sumx.con.
367 inline cic:/CoRN/ftc/Continuity/Continuous_I_Sum.con.
374 For practical purposes, these characterization results are useful:
377 inline cic:/CoRN/ftc/Continuity/lub_charact.con.
379 inline cic:/CoRN/ftc/Continuity/glb_charact.con.
382 The following result is also extremely useful, as it allows us to set a lower bound on the glb of a function.
385 inline cic:/CoRN/ftc/Continuity/leEq_glb.con.
388 The norm is also an extensional property.
391 inline cic:/CoRN/ftc/Continuity/Norm_Funct_wd.con.
394 The value of the norm is covariant with the length of the interval.
397 inline cic:/CoRN/ftc/Continuity/included_imp_norm_leEq.con.
404 Hint Resolve Continuous_I_const Continuous_I_id Continuous_I_plus
405 Continuous_I_inv Continuous_I_minus Continuous_I_mult Continuous_I_scal
406 Continuous_I_recip Continuous_I_max Continuous_I_min Continuous_I_div
407 Continuous_I_nth Continuous_I_abs: continuous.