X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCOrdCauchy.ma;h=14f20ea0266ce0dbfacb77b1093068cfc11b7efb;hb=6f4f26fdfd2a627eef6bf27481e28833df05c82a;hp=37ce37a2210e7d0e3363ee2f17736b0d032daaa1;hpb=0e0d5c57eb154bf20d101f09e560401434156c1d;p=helm.git diff --git a/matita/contribs/CoRN-Decl/algebra/COrdCauchy.ma b/matita/contribs/CoRN-Decl/algebra/COrdCauchy.ma index 37ce37a22..14f20ea02 100644 --- a/matita/contribs/CoRN-Decl/algebra/COrdCauchy.ma +++ b/matita/contribs/CoRN-Decl/algebra/COrdCauchy.ma @@ -16,14 +16,14 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/COrdCauchy". -(* INCLUDE -COrdAbs -*) +include "CoRN.ma". + +include "algebra/COrdAbs.ma". (* Begin_SpecReals *) (* UNEXPORTED -Section OrdField_Cauchy. +Section OrdField_Cauchy *) (*#* **Cauchy sequences @@ -31,7 +31,7 @@ Section OrdField_Cauchy. %\end{convention}% *) -inline cic:/CoRN/algebra/COrdCauchy/R.var. +alias id "R" = "cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/R.var". (* begin hide *) @@ -45,7 +45,7 @@ Unset Strict Implicit. (* end hide *) -inline cic:/CoRN/algebra/COrdCauchy/Cauchy_prop.con. +inline "cic:/CoRN/algebra/COrdCauchy/Cauchy_prop.con". (* begin hide *) @@ -68,9 +68,11 @@ Implicit arguments turned off, because Coq makes a mess of it in combination with the coercions *) -inline cic:/CoRN/algebra/COrdCauchy/CauchySeq.ind. +inline "cic:/CoRN/algebra/COrdCauchy/CauchySeq.ind". + +coercion cic:/matita/CoRN-Decl/algebra/COrdCauchy/CS_seq.con 0 (* compounds *). -inline cic:/CoRN/algebra/COrdCauchy/SeqLimit.con. +inline "cic:/CoRN/algebra/COrdCauchy/SeqLimit.con". (* End_SpecReals *) @@ -84,28 +86,28 @@ hold). %\end{convention}% *) -inline cic:/CoRN/algebra/COrdCauchy/CS_seq_bounded.con. +inline "cic:/CoRN/algebra/COrdCauchy/CS_seq_bounded.con". -inline cic:/CoRN/algebra/COrdCauchy/CS_seq_const.con. +inline "cic:/CoRN/algebra/COrdCauchy/CS_seq_const.con". (*#* %\begin{convention}% Assume [f] and [g] are Cauchy sequences on [R]. %\end{convention}% *) -inline cic:/CoRN/algebra/COrdCauchy/f.var. +alias id "f" = "cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/f.var". -inline cic:/CoRN/algebra/COrdCauchy/g.var. +alias id "g" = "cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/g.var". -inline cic:/CoRN/algebra/COrdCauchy/Hf.var. +alias id "Hf" = "cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/Hf.var". -inline cic:/CoRN/algebra/COrdCauchy/Hg.var. +alias id "Hg" = "cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/Hg.var". -inline cic:/CoRN/algebra/COrdCauchy/CS_seq_plus.con. +inline "cic:/CoRN/algebra/COrdCauchy/CS_seq_plus.con". -inline cic:/CoRN/algebra/COrdCauchy/CS_seq_inv.con. +inline "cic:/CoRN/algebra/COrdCauchy/CS_seq_inv.con". -inline cic:/CoRN/algebra/COrdCauchy/CS_seq_mult.con. +inline "cic:/CoRN/algebra/COrdCauchy/CS_seq_mult.con". (*#* We now assume that [f] is, from some point onwards, greater than @@ -119,22 +121,22 @@ Let [e] be a postive element of [R] and let [N:nat] be such that from %\end{convention}% *) -inline cic:/CoRN/algebra/COrdCauchy/e.var. +alias id "e" = "cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/e.var". -inline cic:/CoRN/algebra/COrdCauchy/He.var. +alias id "He" = "cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/He.var". -inline cic:/CoRN/algebra/COrdCauchy/N.var. +alias id "N" = "cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/N.var". -inline cic:/CoRN/algebra/COrdCauchy/f_bnd.var. +alias id "f_bnd" = "cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/f_bnd.var". -inline cic:/CoRN/algebra/COrdCauchy/CS_seq_recip_def.con. +inline "cic:/CoRN/algebra/COrdCauchy/CS_seq_recip_def.con". -inline cic:/CoRN/algebra/COrdCauchy/CS_seq_recip_seq.con. +inline "cic:/CoRN/algebra/COrdCauchy/CS_seq_recip_seq.con". -inline cic:/CoRN/algebra/COrdCauchy/CS_seq_recip.con. +inline "cic:/CoRN/algebra/COrdCauchy/CS_seq_recip.con". (* UNEXPORTED -End OrdField_Cauchy. +End OrdField_Cauchy *) (* UNEXPORTED @@ -146,13 +148,13 @@ The following lemma does not require the sequence to be Cauchy, but it fits well here anyway. *) -inline cic:/CoRN/algebra/COrdCauchy/maj_upto_eps.con. +inline "cic:/CoRN/algebra/COrdCauchy/maj_upto_eps.con". (* UNEXPORTED -Section Mult_AbsSmall. +Section Mult_AbsSmall *) -inline cic:/CoRN/algebra/COrdCauchy/R.var. +alias id "R" = "cic:/CoRN/algebra/COrdCauchy/Mult_AbsSmall/R.var". (*#* ** [AbsSmall] revisited @@ -160,23 +162,23 @@ inline cic:/CoRN/algebra/COrdCauchy/R.var. %\end{convention}% *) -inline cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall'_rht.con. +inline "cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall'_rht.con". -inline cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall_rht.con. +inline "cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall_rht.con". -inline cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall_lft.con. +inline "cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall_lft.con". -inline cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall.con. +inline "cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall.con". (* UNEXPORTED -End Mult_AbsSmall. +End Mult_AbsSmall *) (* UNEXPORTED -Section Mult_Continuous. +Section Mult_Continuous *) -inline cic:/CoRN/algebra/COrdCauchy/R.var. +alias id "R" = "cic:/CoRN/algebra/COrdCauchy/Mult_Continuous/R.var". (*#* ** Multiplication is continuous @@ -184,22 +186,22 @@ inline cic:/CoRN/algebra/COrdCauchy/R.var. %\end{convention}% *) -inline cic:/CoRN/algebra/COrdCauchy/smaller.con. +inline "cic:/CoRN/algebra/COrdCauchy/smaller.con". -inline cic:/CoRN/algebra/COrdCauchy/estimate_abs.con. +inline "cic:/CoRN/algebra/COrdCauchy/estimate_abs.con". -inline cic:/CoRN/algebra/COrdCauchy/mult_contin.con. +inline "cic:/CoRN/algebra/COrdCauchy/mult_contin.con". (*#* Addition is also continuous. *) -inline cic:/CoRN/algebra/COrdCauchy/plus_contin.con. +inline "cic:/CoRN/algebra/COrdCauchy/plus_contin.con". (* UNEXPORTED -End Mult_Continuous. +End Mult_Continuous *) (* UNEXPORTED -Section Monotonous_functions. +Section Monotonous_functions *) (*#* @@ -212,20 +214,20 @@ characterize them in some way. %\end{convention}% *) -inline cic:/CoRN/algebra/COrdCauchy/R.var. +alias id "R" = "cic:/CoRN/algebra/COrdCauchy/Monotonous_functions/R.var". (*#* We begin by characterizing the preservation of less (less or equal) in terms of preservation of less or equal (less). *) -inline cic:/CoRN/algebra/COrdCauchy/resp_less_char'.con. +inline "cic:/CoRN/algebra/COrdCauchy/resp_less_char'.con". -inline cic:/CoRN/algebra/COrdCauchy/resp_less_char.con. +inline "cic:/CoRN/algebra/COrdCauchy/resp_less_char.con". -inline cic:/CoRN/algebra/COrdCauchy/resp_leEq_char'.con. +inline "cic:/CoRN/algebra/COrdCauchy/resp_leEq_char'.con". -inline cic:/CoRN/algebra/COrdCauchy/resp_leEq_char.con. +inline "cic:/CoRN/algebra/COrdCauchy/resp_leEq_char.con". (*#* Next, we see different characterizations of monotonous functions from @@ -236,47 +238,47 @@ is monotonous iff [f(i) [<] f(i+1)] for every [i]. Also, strictly monotonous functions are injective. *) -inline cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon.con. +inline "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon.con". -inline cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon'.con. +inline "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon'.con". -inline cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'.con. +inline "cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'.con". -inline cic:/CoRN/algebra/COrdCauchy/mon_imp_mon'.con. +inline "cic:/CoRN/algebra/COrdCauchy/mon_imp_mon'.con". -inline cic:/CoRN/algebra/COrdCauchy/mon_imp_inj.con. +inline "cic:/CoRN/algebra/COrdCauchy/mon_imp_inj.con". -inline cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon_lt.con. +inline "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon_lt.con". -inline cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon'_lt.con. +inline "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon'_lt.con". -inline cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'_lt.con. +inline "cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'_lt.con". -inline cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'2_lt.con. +inline "cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'2_lt.con". -inline cic:/CoRN/algebra/COrdCauchy/mon_imp_mon'_lt.con. +inline "cic:/CoRN/algebra/COrdCauchy/mon_imp_mon'_lt.con". -inline cic:/CoRN/algebra/COrdCauchy/mon_imp_inj_lt.con. +inline "cic:/CoRN/algebra/COrdCauchy/mon_imp_inj_lt.con". -inline cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon_le.con. +inline "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon_le.con". -inline cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon'_le.con. +inline "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon'_le.con". -inline cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'_le.con. +inline "cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'_le.con". -inline cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'2_le.con. +inline "cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'2_le.con". -inline cic:/CoRN/algebra/COrdCauchy/mon_imp_mon'_le.con. +inline "cic:/CoRN/algebra/COrdCauchy/mon_imp_mon'_le.con". -inline cic:/CoRN/algebra/COrdCauchy/mon_imp_inj_le.con. +inline "cic:/CoRN/algebra/COrdCauchy/mon_imp_inj_le.con". (*#* A similar result for %{\em %partial%}% functions. *) -inline cic:/CoRN/algebra/COrdCauchy/part_mon_imp_mon'.con. +inline "cic:/CoRN/algebra/COrdCauchy/part_mon_imp_mon'.con". (* UNEXPORTED -End Monotonous_functions. +End Monotonous_functions *)