(**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) (* ||I|| Developers: *) (* ||T|| The HELM team. *) (* ||A|| http://helm.cs.unibo.it *) (* \ / *) (* \ / This file is distributed under the terms of the *) (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) (* This file was automatically generated: do not edit *********************) include "CoRN.ma". (* $Id: Continuity.v,v 1.6 2004/04/23 10:00:58 lcf Exp $ *) (*#* printing Norm_Funct %\ensuremath{\|\cdot\|}% *) include "reals/NRootIR.ma". include "ftc/FunctSums.ma". (* UNEXPORTED Section Definitions_and_Basic_Results *) (*#* *Continuity Constructively, continuity is the most fundamental property of any function---so strongly that no example is known of a constructive function that is not continuous. However, the classical definition of continuity is not good for our purposes, as it is not true, for example, that a function which is continuous in a compact interval is uniformly continuous in that same interval (for a discussion of this see Bishop 1967). Thus, our notion of continuity will be the uniform one#. #%\footnote{%Similar remarks apply to convergence of sequences of functions, which we will define ahead, and elsewhere; we will refrain from discussing this issue at those places.%}.% %\begin{convention}% Throughout this section, [a] and [b] will be real numbers, [I] will denote the compact interval [[a,b]] and [F, G, H] will denote arbitrary partial functions with domains respectively [P, Q] and [R]. %\end{convention}% ** Definitions and Basic Results Here we define continuity and prove some basic properties of continuous functions. *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/a.var *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/b.var *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/Hab.var *) (* begin hide *) inline procedural "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/I.con" "Definitions_and_Basic_Results__" as definition. (* end hide *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/F.var *) (* begin hide *) inline procedural "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/P.con" "Definitions_and_Basic_Results__" as definition. (* end hide *) inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I.con" as definition. (*#* For convenience, we distinguish the two properties of continuous functions. *) inline procedural "cic:/CoRN/ftc/Continuity/contin_imp_inc.con" as lemma. inline procedural "cic:/CoRN/ftc/Continuity/contin_prop.con" as lemma. (*#* Assume [F] to be continuous in [I]. Then it has a least upper bound and a greater lower bound on [I]. *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/contF.var *) (* begin hide *) inline procedural "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/Hinc'.con" "Definitions_and_Basic_Results__" as definition. (* end hide *) inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_imp_tb_image.con" as lemma. inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_imp_lub.con" as lemma. inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_imp_glb.con" as lemma. (*#* We now make this glb and lub into operators. *) inline procedural "cic:/CoRN/ftc/Continuity/lub_funct.con" as definition. inline procedural "cic:/CoRN/ftc/Continuity/glb_funct.con" as definition. (*#* These operators have the expected properties. *) inline procedural "cic:/CoRN/ftc/Continuity/lub_is_lub.con" as lemma. inline procedural "cic:/CoRN/ftc/Continuity/glb_is_glb.con" as lemma. inline procedural "cic:/CoRN/ftc/Continuity/glb_prop.con" as lemma. inline procedural "cic:/CoRN/ftc/Continuity/lub_prop.con" as lemma. (*#* 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). *) inline procedural "cic:/CoRN/ftc/Continuity/Norm_Funct.con" as definition. (*#* The norm effectively bounds the absolute value of a function. *) inline procedural "cic:/CoRN/ftc/Continuity/norm_bnd_AbsIR.con" as lemma. (*#* The following is another way of characterizing the norm: *) inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_imp_abs_lub.con" as lemma. (*#* 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. *) inline procedural "cic:/CoRN/ftc/Continuity/positive_norm.con" as lemma. inline procedural "cic:/CoRN/ftc/Continuity/norm_fun_lub.con" as lemma. inline procedural "cic:/CoRN/ftc/Continuity/leEq_Norm_Funct.con" as lemma. inline procedural "cic:/CoRN/ftc/Continuity/less_Norm_Funct.con" as lemma. (* UNEXPORTED End Definitions_and_Basic_Results *) (* UNEXPORTED Implicit Arguments Continuous_I [a b]. *) (* UNEXPORTED Implicit Arguments Norm_Funct [a b Hab F]. *) (* UNEXPORTED Section Local_Results *) (*#* **Algebraic Properties We now state and prove some results about continuous functions. Assume that [I] is included in the domain of both [F] and [G]. *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Local_Results/a.var *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Local_Results/b.var *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Local_Results/Hab.var *) (* begin hide *) inline procedural "cic:/CoRN/ftc/Continuity/Local_Results/I.con" "Local_Results__" as definition. (* end hide *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Local_Results/F.var *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Local_Results/G.var *) (* begin hide *) inline procedural "cic:/CoRN/ftc/Continuity/Local_Results/P.con" "Local_Results__" as definition. inline procedural "cic:/CoRN/ftc/Continuity/Local_Results/Q.con" "Local_Results__" as definition. (* end hide *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Local_Results/incF.var *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Local_Results/incG.var *) (*#* 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. *) inline procedural "cic:/CoRN/ftc/Continuity/cont_no_sign_change.con" as lemma. inline procedural "cic:/CoRN/ftc/Continuity/cont_no_sign_change_pos.con" as lemma. inline procedural "cic:/CoRN/ftc/Continuity/cont_no_sign_change_neg.con" as lemma. (*#* Being continuous is an extensional property. *) inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_wd.con" as lemma. (*#* A continuous function remains continuous if you restrict its domain. *) inline procedural "cic:/CoRN/ftc/Continuity/included_imp_contin.con" as lemma. (*#* Constant functions and identity are continuous. *) inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_const.con" as lemma. inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_id.con" as lemma. (*#* 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. *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Local_Results/contF.var *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Local_Results/contG.var *) inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_plus.con" as lemma. inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_inv.con" as lemma. inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_mult.con" as lemma. (* UNEXPORTED Opaque AbsIR Max. *) (* UNEXPORTED Transparent AbsIR Max. *) inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_max.con" as lemma. (* begin show *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Local_Results/Hg'.var *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Local_Results/Hg''.var *) (* end show *) inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_recip.con" as lemma. (* UNEXPORTED End Local_Results *) (* UNEXPORTED Hint Resolve contin_imp_inc: included. *) (* UNEXPORTED Section Corolaries *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Corolaries/a.var *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Corolaries/b.var *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Corolaries/Hab.var *) (* begin hide *) inline procedural "cic:/CoRN/ftc/Continuity/Corolaries/I.con" "Corolaries__" as definition. (* end hide *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Corolaries/F.var *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Corolaries/G.var *) (* begin hide *) inline procedural "cic:/CoRN/ftc/Continuity/Corolaries/P.con" "Corolaries__" as definition. inline procedural "cic:/CoRN/ftc/Continuity/Corolaries/Q.con" "Corolaries__" as definition. (* end hide *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Corolaries/contF.var *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Corolaries/contG.var *) (*#* The corresponding properties for subtraction, division and multiplication by a scalar are easily proved as corollaries; exponentiation is proved by induction, appealing to the results on product and constant functions. *) inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_minus.con" as lemma. inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_scal.con" as lemma. inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_nth.con" as lemma. inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_min.con" as lemma. inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_abs.con" as lemma. (* UNEXPORTED cic:/CoRN/ftc/Continuity/Corolaries/Hg'.var *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Corolaries/Hg''.var *) inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_div.con" as lemma. (* UNEXPORTED End Corolaries *) (* UNEXPORTED Section Other *) (* UNEXPORTED Section Sums *) (*#* We finally prove that the sum of an arbitrary family of continuous functions is still a continuous function. *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Other/Sums/a.var *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Other/Sums/b.var *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Other/Sums/Hab.var *) (* UNEXPORTED cic:/CoRN/ftc/Continuity/Other/Sums/Hab'.var *) (* begin hide *) inline procedural "cic:/CoRN/ftc/Continuity/Other/Sums/I.con" "Other__Sums__" as definition. (* end hide *) inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_Sum0.con" as lemma. inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_Sumx.con" as lemma. inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_Sum.con" as lemma. (* UNEXPORTED End Sums *) (*#* For practical purposes, these characterization results are useful: *) inline procedural "cic:/CoRN/ftc/Continuity/lub_charact.con" as lemma. inline procedural "cic:/CoRN/ftc/Continuity/glb_charact.con" as lemma. (*#* The following result is also extremely useful, as it allows us to set a lower bound on the glb of a function. *) inline procedural "cic:/CoRN/ftc/Continuity/leEq_glb.con" as lemma. (*#* The norm is also an extensional property. *) inline procedural "cic:/CoRN/ftc/Continuity/Norm_Funct_wd.con" as lemma. (*#* The value of the norm is covariant with the length of the interval. *) inline procedural "cic:/CoRN/ftc/Continuity/included_imp_norm_leEq.con" as lemma. (* UNEXPORTED End Other *) (* UNEXPORTED Hint Resolve Continuous_I_const Continuous_I_id Continuous_I_plus Continuous_I_inv Continuous_I_minus Continuous_I_mult Continuous_I_scal Continuous_I_recip Continuous_I_max Continuous_I_min Continuous_I_div Continuous_I_nth Continuous_I_abs: continuous. *)