- transcript: patched to generate CoRN_notation.ma instead of CoRN.ma

[helm.git] / helm / software / matita / contribs / CoRN-Decl / ftc / Continuity.ma

diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/Continuity.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/Continuity.ma
index 2ea7152a025134d9e907441fcdc17d0e9969113b..1f205d3e811f33263e6690b8f13ecd2a081f4aa9 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/ftc/Continuity.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/ftc/Continuity.ma
@@ -16,17 +16,15 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/ftc/Continuity".
 
+include "CoRN_notation.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.
@@ -56,103 +54,103 @@ respectively [P, Q] and [R].
 Here we define continuity and prove some basic properties of continuous functions.
 *)
 
-inline cic:/CoRN/ftc/Continuity/a.var.
+inline "cic:/CoRN/ftc/Continuity/a.var".
 
-inline cic:/CoRN/ftc/Continuity/b.var.
+inline "cic:/CoRN/ftc/Continuity/b.var".
 
-inline cic:/CoRN/ftc/Continuity/Hab.var.
+inline "cic:/CoRN/ftc/Continuity/Hab.var".
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/Continuity/I.con.
+inline "cic:/CoRN/ftc/Continuity/I.con".
 
 (* end hide *)
 
-inline cic:/CoRN/ftc/Continuity/F.var.
+inline "cic:/CoRN/ftc/Continuity/F.var".
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/Continuity/P.con.
+inline "cic:/CoRN/ftc/Continuity/P.con".
 
 (* 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.
+inline "cic:/CoRN/ftc/Continuity/contF.var".
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/Continuity/Hinc'.con.
+inline "cic:/CoRN/ftc/Continuity/Hinc'.con".
 
 (* 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.
@@ -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.
+inline "cic:/CoRN/ftc/Continuity/a.var".
 
-inline cic:/CoRN/ftc/Continuity/b.var.
+inline "cic:/CoRN/ftc/Continuity/b.var".
 
-inline cic:/CoRN/ftc/Continuity/Hab.var.
+inline "cic:/CoRN/ftc/Continuity/Hab.var".
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/Continuity/I.con.
+inline "cic:/CoRN/ftc/Continuity/I.con".
 
 (* end hide *)
 
-inline cic:/CoRN/ftc/Continuity/F.var.
+inline "cic:/CoRN/ftc/Continuity/F.var".
 
-inline cic:/CoRN/ftc/Continuity/G.var.
+inline "cic:/CoRN/ftc/Continuity/G.var".
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/Continuity/P.con.
+inline "cic:/CoRN/ftc/Continuity/P.con".
 
-inline cic:/CoRN/ftc/Continuity/Q.con.
+inline "cic:/CoRN/ftc/Continuity/Q.con".
 
 (* end hide *)
 
-inline cic:/CoRN/ftc/Continuity/incF.var.
+inline "cic:/CoRN/ftc/Continuity/incF.var".
 
-inline cic:/CoRN/ftc/Continuity/incG.var.
+inline "cic:/CoRN/ftc/Continuity/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.
+inline "cic:/CoRN/ftc/Continuity/contF.var".
 
-inline cic:/CoRN/ftc/Continuity/contG.var.
+inline "cic:/CoRN/ftc/Continuity/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,17 +253,17 @@ 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.
+inline "cic:/CoRN/ftc/Continuity/Hg'.var".
 
-inline cic:/CoRN/ftc/Continuity/Hg''.var.
+inline "cic:/CoRN/ftc/Continuity/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.
@@ -279,33 +277,33 @@ Hint Resolve contin_imp_inc: included.
 Section Corolaries.
 *)
 
-inline cic:/CoRN/ftc/Continuity/a.var.
+inline "cic:/CoRN/ftc/Continuity/a.var".
 
-inline cic:/CoRN/ftc/Continuity/b.var.
+inline "cic:/CoRN/ftc/Continuity/b.var".
 
-inline cic:/CoRN/ftc/Continuity/Hab.var.
+inline "cic:/CoRN/ftc/Continuity/Hab.var".
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/Continuity/I.con.
+inline "cic:/CoRN/ftc/Continuity/I.con".
 
 (* end hide *)
 
-inline cic:/CoRN/ftc/Continuity/F.var.
+inline "cic:/CoRN/ftc/Continuity/F.var".
 
-inline cic:/CoRN/ftc/Continuity/G.var.
+inline "cic:/CoRN/ftc/Continuity/G.var".
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/Continuity/P.con.
+inline "cic:/CoRN/ftc/Continuity/P.con".
 
-inline cic:/CoRN/ftc/Continuity/Q.con.
+inline "cic:/CoRN/ftc/Continuity/Q.con".
 
 (* end hide *)
 
-inline cic:/CoRN/ftc/Continuity/contF.var.
+inline "cic:/CoRN/ftc/Continuity/contF.var".
 
-inline cic:/CoRN/ftc/Continuity/contG.var.
+inline "cic:/CoRN/ftc/Continuity/contG.var".
 
 (*#*
 The corresponding properties for subtraction, division and
@@ -314,21 +312,21 @@ 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.
+inline "cic:/CoRN/ftc/Continuity/Hg'.var".
 
-inline cic:/CoRN/ftc/Continuity/Hg''.var.
+inline "cic:/CoRN/ftc/Continuity/Hg''.var".
 
-inline cic:/CoRN/ftc/Continuity/Continuous_I_div.con.
+inline "cic:/CoRN/ftc/Continuity/Continuous_I_div.con".
 
 (* UNEXPORTED
 End Corolaries.
@@ -346,25 +344,25 @@ 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.
+inline "cic:/CoRN/ftc/Continuity/a.var".
 
-inline cic:/CoRN/ftc/Continuity/b.var.
+inline "cic:/CoRN/ftc/Continuity/b.var".
 
-inline cic:/CoRN/ftc/Continuity/Hab.var.
+inline "cic:/CoRN/ftc/Continuity/Hab.var".
 
-inline cic:/CoRN/ftc/Continuity/Hab'.var.
+inline "cic:/CoRN/ftc/Continuity/Hab'.var".
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/Continuity/I.con.
+inline "cic:/CoRN/ftc/Continuity/I.con".
 
 (* 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.
@@ -374,27 +372,27 @@ 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.