X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Fftc%2FContinuity.ma;h=6f884860a89430f04a5213043618cb2701204196;hb=0a9ed4329c069d2e06902934b6d1d58d3690959c;hp=2ea7152a025134d9e907441fcdc17d0e9969113b;hpb=0e0d5c57eb154bf20d101f09e560401434156c1d;p=helm.git diff --git a/matita/contribs/CoRN-Decl/ftc/Continuity.ma b/matita/contribs/CoRN-Decl/ftc/Continuity.ma index 2ea7152a0..6f884860a 100644 --- a/matita/contribs/CoRN-Decl/ftc/Continuity.ma +++ b/matita/contribs/CoRN-Decl/ftc/Continuity.ma @@ -16,20 +16,18 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/Continuity". +include "CoRN.ma". + (* $Id: Continuity.v,v 1.6 2004/04/23 10:00:58 lcf Exp $ *) (*#* printing Norm_Funct %\ensuremath{\|\cdot\|}% *) -(* INCLUDE -NRootIR -*) +include "reals/NRootIR.ma". -(* INCLUDE -FunctSums -*) +include "ftc/FunctSums.ma". (* UNEXPORTED -Section Definitions_and_Basic_Results. +Section Definitions_and_Basic_Results *) (*#* *Continuity @@ -56,106 +54,106 @@ respectively [P, Q] and [R]. Here we define continuity and prove some basic properties of continuous functions. *) -inline cic:/CoRN/ftc/Continuity/a.var. +alias id "a" = "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/a.var". -inline cic:/CoRN/ftc/Continuity/b.var. +alias id "b" = "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/b.var". -inline cic:/CoRN/ftc/Continuity/Hab.var. +alias id "Hab" = "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/Hab.var". (* begin hide *) -inline cic:/CoRN/ftc/Continuity/I.con. +inline "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/I.con" "Definitions_and_Basic_Results__". (* end hide *) -inline cic:/CoRN/ftc/Continuity/F.var. +alias id "F" = "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/F.var". (* begin hide *) -inline cic:/CoRN/ftc/Continuity/P.con. +inline "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/P.con" "Definitions_and_Basic_Results__". (* end hide *) -inline cic:/CoRN/ftc/Continuity/Continuous_I.con. +inline "cic:/CoRN/ftc/Continuity/Continuous_I.con". (*#* For convenience, we distinguish the two properties of continuous functions. *) -inline cic:/CoRN/ftc/Continuity/contin_imp_inc.con. +inline "cic:/CoRN/ftc/Continuity/contin_imp_inc.con". -inline cic:/CoRN/ftc/Continuity/contin_prop.con. +inline "cic:/CoRN/ftc/Continuity/contin_prop.con". (*#* Assume [F] to be continuous in [I]. Then it has a least upper bound and a greater lower bound on [I]. *) -inline cic:/CoRN/ftc/Continuity/contF.var. +alias id "contF" = "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/contF.var". (* begin hide *) -inline cic:/CoRN/ftc/Continuity/Hinc'.con. +inline "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/Hinc'.con" "Definitions_and_Basic_Results__". (* end hide *) -inline cic:/CoRN/ftc/Continuity/Continuous_I_imp_tb_image.con. +inline "cic:/CoRN/ftc/Continuity/Continuous_I_imp_tb_image.con". -inline cic:/CoRN/ftc/Continuity/Continuous_I_imp_lub.con. +inline "cic:/CoRN/ftc/Continuity/Continuous_I_imp_lub.con". -inline cic:/CoRN/ftc/Continuity/Continuous_I_imp_glb.con. +inline "cic:/CoRN/ftc/Continuity/Continuous_I_imp_glb.con". (*#* We now make this glb and lub into operators. *) -inline cic:/CoRN/ftc/Continuity/lub_funct.con. +inline "cic:/CoRN/ftc/Continuity/lub_funct.con". -inline cic:/CoRN/ftc/Continuity/glb_funct.con. +inline "cic:/CoRN/ftc/Continuity/glb_funct.con". (*#* These operators have the expected properties. *) -inline cic:/CoRN/ftc/Continuity/lub_is_lub.con. +inline "cic:/CoRN/ftc/Continuity/lub_is_lub.con". -inline cic:/CoRN/ftc/Continuity/glb_is_glb.con. +inline "cic:/CoRN/ftc/Continuity/glb_is_glb.con". -inline cic:/CoRN/ftc/Continuity/glb_prop.con. +inline "cic:/CoRN/ftc/Continuity/glb_prop.con". -inline cic:/CoRN/ftc/Continuity/lub_prop.con. +inline "cic:/CoRN/ftc/Continuity/lub_prop.con". (*#* 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 cic:/CoRN/ftc/Continuity/Norm_Funct.con. +inline "cic:/CoRN/ftc/Continuity/Norm_Funct.con". (*#* The norm effectively bounds the absolute value of a function. *) -inline cic:/CoRN/ftc/Continuity/norm_bnd_AbsIR.con. +inline "cic:/CoRN/ftc/Continuity/norm_bnd_AbsIR.con". (*#* The following is another way of characterizing the norm: *) -inline cic:/CoRN/ftc/Continuity/Continuous_I_imp_abs_lub.con. +inline "cic:/CoRN/ftc/Continuity/Continuous_I_imp_abs_lub.con". (*#* 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 cic:/CoRN/ftc/Continuity/positive_norm.con. +inline "cic:/CoRN/ftc/Continuity/positive_norm.con". -inline cic:/CoRN/ftc/Continuity/norm_fun_lub.con. +inline "cic:/CoRN/ftc/Continuity/norm_fun_lub.con". -inline cic:/CoRN/ftc/Continuity/leEq_Norm_Funct.con. +inline "cic:/CoRN/ftc/Continuity/leEq_Norm_Funct.con". -inline cic:/CoRN/ftc/Continuity/less_Norm_Funct.con. +inline "cic:/CoRN/ftc/Continuity/less_Norm_Funct.con". (* UNEXPORTED -End Definitions_and_Basic_Results. +End Definitions_and_Basic_Results *) (* UNEXPORTED @@ -167,7 +165,7 @@ Implicit Arguments Norm_Funct [a b Hab F]. *) (* UNEXPORTED -Section Local_Results. +Section Local_Results *) (*#* **Algebraic Properties @@ -175,77 +173,77 @@ Section Local_Results. We now state and prove some results about continuous functions. Assume that [I] is included in the domain of both [F] and [G]. *) -inline cic:/CoRN/ftc/Continuity/a.var. +alias id "a" = "cic:/CoRN/ftc/Continuity/Local_Results/a.var". -inline cic:/CoRN/ftc/Continuity/b.var. +alias id "b" = "cic:/CoRN/ftc/Continuity/Local_Results/b.var". -inline cic:/CoRN/ftc/Continuity/Hab.var. +alias id "Hab" = "cic:/CoRN/ftc/Continuity/Local_Results/Hab.var". (* begin hide *) -inline cic:/CoRN/ftc/Continuity/I.con. +inline "cic:/CoRN/ftc/Continuity/Local_Results/I.con" "Local_Results__". (* end hide *) -inline cic:/CoRN/ftc/Continuity/F.var. +alias id "F" = "cic:/CoRN/ftc/Continuity/Local_Results/F.var". -inline cic:/CoRN/ftc/Continuity/G.var. +alias id "G" = "cic:/CoRN/ftc/Continuity/Local_Results/G.var". (* begin hide *) -inline cic:/CoRN/ftc/Continuity/P.con. +inline "cic:/CoRN/ftc/Continuity/Local_Results/P.con" "Local_Results__". -inline cic:/CoRN/ftc/Continuity/Q.con. +inline "cic:/CoRN/ftc/Continuity/Local_Results/Q.con" "Local_Results__". (* end hide *) -inline cic:/CoRN/ftc/Continuity/incF.var. +alias id "incF" = "cic:/CoRN/ftc/Continuity/Local_Results/incF.var". -inline cic:/CoRN/ftc/Continuity/incG.var. +alias id "incG" = "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 cic:/CoRN/ftc/Continuity/cont_no_sign_change.con. +inline "cic:/CoRN/ftc/Continuity/cont_no_sign_change.con". -inline cic:/CoRN/ftc/Continuity/cont_no_sign_change_pos.con. +inline "cic:/CoRN/ftc/Continuity/cont_no_sign_change_pos.con". -inline cic:/CoRN/ftc/Continuity/cont_no_sign_change_neg.con. +inline "cic:/CoRN/ftc/Continuity/cont_no_sign_change_neg.con". (*#* Being continuous is an extensional property. *) -inline cic:/CoRN/ftc/Continuity/Continuous_I_wd.con. +inline "cic:/CoRN/ftc/Continuity/Continuous_I_wd.con". (*#* A continuous function remains continuous if you restrict its domain. *) -inline cic:/CoRN/ftc/Continuity/included_imp_contin.con. +inline "cic:/CoRN/ftc/Continuity/included_imp_contin.con". (*#* Constant functions and identity are continuous. *) -inline cic:/CoRN/ftc/Continuity/Continuous_I_const.con. +inline "cic:/CoRN/ftc/Continuity/Continuous_I_const.con". -inline cic:/CoRN/ftc/Continuity/Continuous_I_id.con. +inline "cic:/CoRN/ftc/Continuity/Continuous_I_id.con". (*#* 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. *) -inline cic:/CoRN/ftc/Continuity/contF.var. +alias id "contF" = "cic:/CoRN/ftc/Continuity/Local_Results/contF.var". -inline cic:/CoRN/ftc/Continuity/contG.var. +alias id "contG" = "cic:/CoRN/ftc/Continuity/Local_Results/contG.var". -inline cic:/CoRN/ftc/Continuity/Continuous_I_plus.con. +inline "cic:/CoRN/ftc/Continuity/Continuous_I_plus.con". -inline cic:/CoRN/ftc/Continuity/Continuous_I_inv.con. +inline "cic:/CoRN/ftc/Continuity/Continuous_I_inv.con". -inline cic:/CoRN/ftc/Continuity/Continuous_I_mult.con. +inline "cic:/CoRN/ftc/Continuity/Continuous_I_mult.con". (* UNEXPORTED Opaque AbsIR Max. @@ -255,20 +253,20 @@ Opaque AbsIR Max. Transparent AbsIR Max. *) -inline cic:/CoRN/ftc/Continuity/Continuous_I_max.con. +inline "cic:/CoRN/ftc/Continuity/Continuous_I_max.con". (* begin show *) -inline cic:/CoRN/ftc/Continuity/Hg'.var. +alias id "Hg'" = "cic:/CoRN/ftc/Continuity/Local_Results/Hg'.var". -inline cic:/CoRN/ftc/Continuity/Hg''.var. +alias id "Hg''" = "cic:/CoRN/ftc/Continuity/Local_Results/Hg''.var". (* end show *) -inline cic:/CoRN/ftc/Continuity/Continuous_I_recip.con. +inline "cic:/CoRN/ftc/Continuity/Continuous_I_recip.con". (* UNEXPORTED -End Local_Results. +End Local_Results *) (* UNEXPORTED @@ -276,36 +274,36 @@ Hint Resolve contin_imp_inc: included. *) (* UNEXPORTED -Section Corolaries. +Section Corolaries *) -inline cic:/CoRN/ftc/Continuity/a.var. +alias id "a" = "cic:/CoRN/ftc/Continuity/Corolaries/a.var". -inline cic:/CoRN/ftc/Continuity/b.var. +alias id "b" = "cic:/CoRN/ftc/Continuity/Corolaries/b.var". -inline cic:/CoRN/ftc/Continuity/Hab.var. +alias id "Hab" = "cic:/CoRN/ftc/Continuity/Corolaries/Hab.var". (* begin hide *) -inline cic:/CoRN/ftc/Continuity/I.con. +inline "cic:/CoRN/ftc/Continuity/Corolaries/I.con" "Corolaries__". (* end hide *) -inline cic:/CoRN/ftc/Continuity/F.var. +alias id "F" = "cic:/CoRN/ftc/Continuity/Corolaries/F.var". -inline cic:/CoRN/ftc/Continuity/G.var. +alias id "G" = "cic:/CoRN/ftc/Continuity/Corolaries/G.var". (* begin hide *) -inline cic:/CoRN/ftc/Continuity/P.con. +inline "cic:/CoRN/ftc/Continuity/Corolaries/P.con" "Corolaries__". -inline cic:/CoRN/ftc/Continuity/Q.con. +inline "cic:/CoRN/ftc/Continuity/Corolaries/Q.con" "Corolaries__". (* end hide *) -inline cic:/CoRN/ftc/Continuity/contF.var. +alias id "contF" = "cic:/CoRN/ftc/Continuity/Corolaries/contF.var". -inline cic:/CoRN/ftc/Continuity/contG.var. +alias id "contG" = "cic:/CoRN/ftc/Continuity/Corolaries/contG.var". (*#* The corresponding properties for subtraction, division and @@ -314,90 +312,90 @@ exponentiation is proved by induction, appealing to the results on product and constant functions. *) -inline cic:/CoRN/ftc/Continuity/Continuous_I_minus.con. +inline "cic:/CoRN/ftc/Continuity/Continuous_I_minus.con". -inline cic:/CoRN/ftc/Continuity/Continuous_I_scal.con. +inline "cic:/CoRN/ftc/Continuity/Continuous_I_scal.con". -inline cic:/CoRN/ftc/Continuity/Continuous_I_nth.con. +inline "cic:/CoRN/ftc/Continuity/Continuous_I_nth.con". -inline cic:/CoRN/ftc/Continuity/Continuous_I_min.con. +inline "cic:/CoRN/ftc/Continuity/Continuous_I_min.con". -inline cic:/CoRN/ftc/Continuity/Continuous_I_abs.con. +inline "cic:/CoRN/ftc/Continuity/Continuous_I_abs.con". -inline cic:/CoRN/ftc/Continuity/Hg'.var. +alias id "Hg'" = "cic:/CoRN/ftc/Continuity/Corolaries/Hg'.var". -inline cic:/CoRN/ftc/Continuity/Hg''.var. +alias id "Hg''" = "cic:/CoRN/ftc/Continuity/Corolaries/Hg''.var". -inline cic:/CoRN/ftc/Continuity/Continuous_I_div.con. +inline "cic:/CoRN/ftc/Continuity/Continuous_I_div.con". (* UNEXPORTED -End Corolaries. +End Corolaries *) (* UNEXPORTED -Section Other. +Section Other *) (* UNEXPORTED -Section Sums. +Section Sums *) (*#* We finally prove that the sum of an arbitrary family of continuous functions is still a continuous function. *) -inline cic:/CoRN/ftc/Continuity/a.var. +alias id "a" = "cic:/CoRN/ftc/Continuity/Other/Sums/a.var". -inline cic:/CoRN/ftc/Continuity/b.var. +alias id "b" = "cic:/CoRN/ftc/Continuity/Other/Sums/b.var". -inline cic:/CoRN/ftc/Continuity/Hab.var. +alias id "Hab" = "cic:/CoRN/ftc/Continuity/Other/Sums/Hab.var". -inline cic:/CoRN/ftc/Continuity/Hab'.var. +alias id "Hab'" = "cic:/CoRN/ftc/Continuity/Other/Sums/Hab'.var". (* begin hide *) -inline cic:/CoRN/ftc/Continuity/I.con. +inline "cic:/CoRN/ftc/Continuity/Other/Sums/I.con" "Other__Sums__". (* end hide *) -inline cic:/CoRN/ftc/Continuity/Continuous_I_Sum0.con. +inline "cic:/CoRN/ftc/Continuity/Continuous_I_Sum0.con". -inline cic:/CoRN/ftc/Continuity/Continuous_I_Sumx.con. +inline "cic:/CoRN/ftc/Continuity/Continuous_I_Sumx.con". -inline cic:/CoRN/ftc/Continuity/Continuous_I_Sum.con. +inline "cic:/CoRN/ftc/Continuity/Continuous_I_Sum.con". (* UNEXPORTED -End Sums. +End Sums *) (*#* For practical purposes, these characterization results are useful: *) -inline cic:/CoRN/ftc/Continuity/lub_charact.con. +inline "cic:/CoRN/ftc/Continuity/lub_charact.con". -inline cic:/CoRN/ftc/Continuity/glb_charact.con. +inline "cic:/CoRN/ftc/Continuity/glb_charact.con". (*#* The following result is also extremely useful, as it allows us to set a lower bound on the glb of a function. *) -inline cic:/CoRN/ftc/Continuity/leEq_glb.con. +inline "cic:/CoRN/ftc/Continuity/leEq_glb.con". (*#* The norm is also an extensional property. *) -inline cic:/CoRN/ftc/Continuity/Norm_Funct_wd.con. +inline "cic:/CoRN/ftc/Continuity/Norm_Funct_wd.con". (*#* The value of the norm is covariant with the length of the interval. *) -inline cic:/CoRN/ftc/Continuity/included_imp_norm_leEq.con. +inline "cic:/CoRN/ftc/Continuity/included_imp_norm_leEq.con". (* UNEXPORTED -End Other. +End Other *) (* UNEXPORTED