X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FFunctSequence.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FFunctSequence.ma;h=768b71285917bea80f9068c4e26f705bc9867bb3;hb=80110e17ef1d38d71473e9471ce15beddde663bb;hp=c5c588036cb58fda9873de6e0de8fe2c039c7248;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSequence.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSequence.ma index c5c588036..768b71285 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSequence.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/FunctSequence.ma @@ -16,15 +16,13 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/FunctSequence". +include "CoRN.ma". + (* $Id: FunctSequence.v,v 1.5 2004/04/23 10:00:58 lcf Exp $ *) -(* INCLUDE -Continuity -*) +include "ftc/Continuity.ma". -(* INCLUDE -PartInterval -*) +include "ftc/PartInterval.ma". (* UNEXPORTED Section Definitions. @@ -54,77 +52,77 @@ be defined. For a discussion on the different notions of convergent see Bishop 1967. *) -inline cic:/CoRN/ftc/FunctSequence/a.var. +inline "cic:/CoRN/ftc/FunctSequence/a.var". -inline cic:/CoRN/ftc/FunctSequence/b.var. +inline "cic:/CoRN/ftc/FunctSequence/b.var". -inline cic:/CoRN/ftc/FunctSequence/Hab.var. +inline "cic:/CoRN/ftc/FunctSequence/Hab.var". (* begin hide *) -inline cic:/CoRN/ftc/FunctSequence/I.con. +inline "cic:/CoRN/ftc/FunctSequence/I.con". (* end hide *) -inline cic:/CoRN/ftc/FunctSequence/f.var. +inline "cic:/CoRN/ftc/FunctSequence/f.var". -inline cic:/CoRN/ftc/FunctSequence/F.var. +inline "cic:/CoRN/ftc/FunctSequence/F.var". -inline cic:/CoRN/ftc/FunctSequence/contf.var. +inline "cic:/CoRN/ftc/FunctSequence/contf.var". -inline cic:/CoRN/ftc/FunctSequence/contF.var. +inline "cic:/CoRN/ftc/FunctSequence/contF.var". (* begin hide *) -inline cic:/CoRN/ftc/FunctSequence/incf.con. +inline "cic:/CoRN/ftc/FunctSequence/incf.con". -inline cic:/CoRN/ftc/FunctSequence/incF.con. +inline "cic:/CoRN/ftc/FunctSequence/incF.con". (* end hide *) -inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq.con. +inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq.con". -inline cic:/CoRN/ftc/FunctSequence/conv_fun_seq'.con. +inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'.con". -inline cic:/CoRN/ftc/FunctSequence/conv_norm_fun_seq.con. +inline "cic:/CoRN/ftc/FunctSequence/conv_norm_fun_seq.con". -inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1.con. +inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1.con". -inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'.con. +inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'.con". -inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2.con. +inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2.con". (*#* These definitions are all shown to be equivalent. *) -inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq'.con. +inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq'.con". -inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_seq.con. +inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_seq.con". -inline cic:/CoRN/ftc/FunctSequence/conv_Cauchy_fun_seq'.con. +inline "cic:/CoRN/ftc/FunctSequence/conv_Cauchy_fun_seq'.con". -inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq2.con. +inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq2.con". -inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2_seq.con. +inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2_seq.con". -inline cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_norm.con. +inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_norm.con". -inline cic:/CoRN/ftc/FunctSequence/conv_fun_norm_seq.con. +inline "cic:/CoRN/ftc/FunctSequence/conv_fun_norm_seq.con". -inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_seq'.con. +inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_seq'.con". -inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_seq1.con. +inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_seq1.con". -inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq1.con. +inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq1.con". -inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_seq.con. +inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_seq.con". (*#* A Cauchy sequence of functions is pointwise a Cauchy sequence. *) -inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_real.con. +inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_real.con". (* UNEXPORTED End Definitions. @@ -134,21 +132,21 @@ End Definitions. Section More_Definitions. *) -inline cic:/CoRN/ftc/FunctSequence/a.var. +inline "cic:/CoRN/ftc/FunctSequence/a.var". -inline cic:/CoRN/ftc/FunctSequence/b.var. +inline "cic:/CoRN/ftc/FunctSequence/b.var". -inline cic:/CoRN/ftc/FunctSequence/Hab.var. +inline "cic:/CoRN/ftc/FunctSequence/Hab.var". (* begin hide *) -inline cic:/CoRN/ftc/FunctSequence/I.con. +inline "cic:/CoRN/ftc/FunctSequence/I.con". (* end hide *) -inline cic:/CoRN/ftc/FunctSequence/f.var. +inline "cic:/CoRN/ftc/FunctSequence/f.var". -inline cic:/CoRN/ftc/FunctSequence/contf.var. +inline "cic:/CoRN/ftc/FunctSequence/contf.var". (*#* We can also say that [f] is simply convergent if it converges to some @@ -156,7 +154,7 @@ continuous function. Notice that we do not quantify directly over partial functions, for reasons which were already explained. *) -inline cic:/CoRN/ftc/FunctSequence/conv_fun_seq.con. +inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq.con". (*#* It is useful to extract the limit as a partial function: @@ -164,11 +162,11 @@ It is useful to extract the limit as a partial function: (* begin show *) -inline cic:/CoRN/ftc/FunctSequence/H.var. +inline "cic:/CoRN/ftc/FunctSequence/H.var". (* end show *) -inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_Lim.con. +inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_Lim.con". (* UNEXPORTED End More_Definitions. @@ -183,47 +181,47 @@ Section Irrelevance_of_Proofs. This section contains a number of technical results stating mainly that being a Cauchy sequence or converging to some limit is a property of the sequence itself and independent of the proofs we supply of its continuity or the continuity of its limit. *) -inline cic:/CoRN/ftc/FunctSequence/a.var. +inline "cic:/CoRN/ftc/FunctSequence/a.var". -inline cic:/CoRN/ftc/FunctSequence/b.var. +inline "cic:/CoRN/ftc/FunctSequence/b.var". -inline cic:/CoRN/ftc/FunctSequence/Hab.var. +inline "cic:/CoRN/ftc/FunctSequence/Hab.var". (* begin hide *) -inline cic:/CoRN/ftc/FunctSequence/I.con. +inline "cic:/CoRN/ftc/FunctSequence/I.con". (* end hide *) -inline cic:/CoRN/ftc/FunctSequence/f.var. +inline "cic:/CoRN/ftc/FunctSequence/f.var". (* begin show *) -inline cic:/CoRN/ftc/FunctSequence/contf.var. +inline "cic:/CoRN/ftc/FunctSequence/contf.var". -inline cic:/CoRN/ftc/FunctSequence/contf0.var. +inline "cic:/CoRN/ftc/FunctSequence/contf0.var". (* end show *) -inline cic:/CoRN/ftc/FunctSequence/F.var. +inline "cic:/CoRN/ftc/FunctSequence/F.var". (* begin show *) -inline cic:/CoRN/ftc/FunctSequence/contF.var. +inline "cic:/CoRN/ftc/FunctSequence/contF.var". -inline cic:/CoRN/ftc/FunctSequence/contF0.var. +inline "cic:/CoRN/ftc/FunctSequence/contF0.var". (* end show *) -inline cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wd.con. +inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wd.con". -inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_wd.con. +inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_wd.con". -inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2_wd.con. +inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2_wd.con". -inline cic:/CoRN/ftc/FunctSequence/conv_norm_fun_seq_wd.con. +inline "cic:/CoRN/ftc/FunctSequence/conv_norm_fun_seq_wd.con". -inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_wd.con. +inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_wd.con". (* UNEXPORTED End Irrelevance_of_Proofs. @@ -233,7 +231,7 @@ End Irrelevance_of_Proofs. Section More_Proof_Irrelevance. *) -inline cic:/CoRN/ftc/FunctSequence/conv_fun_seq_wd.con. +inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq_wd.con". (* UNEXPORTED End More_Proof_Irrelevance. @@ -250,79 +248,79 @@ limit; the limit is a continuous function; and convergence is well defined with respect to functional equality in the interval [[a,b]]. *) -inline cic:/CoRN/ftc/FunctSequence/a.var. +inline "cic:/CoRN/ftc/FunctSequence/a.var". -inline cic:/CoRN/ftc/FunctSequence/b.var. +inline "cic:/CoRN/ftc/FunctSequence/b.var". -inline cic:/CoRN/ftc/FunctSequence/Hab.var. +inline "cic:/CoRN/ftc/FunctSequence/Hab.var". (* begin hide *) -inline cic:/CoRN/ftc/FunctSequence/I.con. +inline "cic:/CoRN/ftc/FunctSequence/I.con". (* end hide *) -inline cic:/CoRN/ftc/FunctSequence/f.var. +inline "cic:/CoRN/ftc/FunctSequence/f.var". -inline cic:/CoRN/ftc/FunctSequence/g.var. +inline "cic:/CoRN/ftc/FunctSequence/g.var". (* begin show *) -inline cic:/CoRN/ftc/FunctSequence/contf.var. +inline "cic:/CoRN/ftc/FunctSequence/contf.var". -inline cic:/CoRN/ftc/FunctSequence/contf0.var. +inline "cic:/CoRN/ftc/FunctSequence/contf0.var". -inline cic:/CoRN/ftc/FunctSequence/contg.var. +inline "cic:/CoRN/ftc/FunctSequence/contg.var". -inline cic:/CoRN/ftc/FunctSequence/contg0.var. +inline "cic:/CoRN/ftc/FunctSequence/contg0.var". (* end show *) -inline cic:/CoRN/ftc/FunctSequence/Cauchy_conv_fun_seq'.con. +inline "cic:/CoRN/ftc/FunctSequence/Cauchy_conv_fun_seq'.con". -inline cic:/CoRN/ftc/FunctSequence/F.var. +inline "cic:/CoRN/ftc/FunctSequence/F.var". -inline cic:/CoRN/ftc/FunctSequence/G.var. +inline "cic:/CoRN/ftc/FunctSequence/G.var". (* begin show *) -inline cic:/CoRN/ftc/FunctSequence/contF.var. +inline "cic:/CoRN/ftc/FunctSequence/contF.var". -inline cic:/CoRN/ftc/FunctSequence/contF0.var. +inline "cic:/CoRN/ftc/FunctSequence/contF0.var". -inline cic:/CoRN/ftc/FunctSequence/contG.var. +inline "cic:/CoRN/ftc/FunctSequence/contG.var". -inline cic:/CoRN/ftc/FunctSequence/contG0.var. +inline "cic:/CoRN/ftc/FunctSequence/contG0.var". (* end show *) -inline cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdl.con. +inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdl.con". -inline cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdr.con. +inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdr.con". -inline cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdl'.con. +inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdl'.con". -inline cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdr'.con. +inline "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdr'.con". -inline cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_wd.con. +inline "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_wd.con". -inline cic:/CoRN/ftc/FunctSequence/Cauchy_cont_Lim.con. +inline "cic:/CoRN/ftc/FunctSequence/Cauchy_cont_Lim.con". -inline cic:/CoRN/ftc/FunctSequence/Cauchy_conv_fun_seq.con. +inline "cic:/CoRN/ftc/FunctSequence/Cauchy_conv_fun_seq.con". -inline cic:/CoRN/ftc/FunctSequence/conv_Cauchy_fun_seq.con. +inline "cic:/CoRN/ftc/FunctSequence/conv_Cauchy_fun_seq.con". (*#* More interesting is the fact that a convergent sequence of functions converges pointwise as a sequence of real numbers. *) -inline cic:/CoRN/ftc/FunctSequence/fun_conv_imp_seq_conv.con. +inline "cic:/CoRN/ftc/FunctSequence/fun_conv_imp_seq_conv.con". (*#* And a sequence of real numbers converges iff the corresponding sequence of constant functions converges to the corresponding constant function. *) -inline cic:/CoRN/ftc/FunctSequence/seq_conv_imp_fun_conv.con. +inline "cic:/CoRN/ftc/FunctSequence/seq_conv_imp_fun_conv.con". (* UNEXPORTED End More_Properties. @@ -341,76 +339,76 @@ Section Algebraic_Properties. We now study how convergence is affected by algebraic operations, and some algebraic properties of the limit function. *) -inline cic:/CoRN/ftc/FunctSequence/a.var. +inline "cic:/CoRN/ftc/FunctSequence/a.var". -inline cic:/CoRN/ftc/FunctSequence/b.var. +inline "cic:/CoRN/ftc/FunctSequence/b.var". -inline cic:/CoRN/ftc/FunctSequence/Hab.var. +inline "cic:/CoRN/ftc/FunctSequence/Hab.var". (* begin hide *) -inline cic:/CoRN/ftc/FunctSequence/I.con. +inline "cic:/CoRN/ftc/FunctSequence/I.con". (* end hide *) -inline cic:/CoRN/ftc/FunctSequence/f.var. +inline "cic:/CoRN/ftc/FunctSequence/f.var". -inline cic:/CoRN/ftc/FunctSequence/g.var. +inline "cic:/CoRN/ftc/FunctSequence/g.var". -inline cic:/CoRN/ftc/FunctSequence/contf.var. +inline "cic:/CoRN/ftc/FunctSequence/contf.var". -inline cic:/CoRN/ftc/FunctSequence/contg.var. +inline "cic:/CoRN/ftc/FunctSequence/contg.var". (*#* First, the limit function is unique. *) -inline cic:/CoRN/ftc/FunctSequence/FLim_unique.con. +inline "cic:/CoRN/ftc/FunctSequence/FLim_unique.con". (*#* Constant sequences (not sequences of constant functions!) always converge. *) -inline cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_const.con. +inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_const.con". -inline cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_const.con. +inline "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_const.con". (*#* We now prove that if two sequences converge than their sum (difference, product) also converge to the sum (difference, product) of their limits. *) -inline cic:/CoRN/ftc/FunctSequence/F.var. +inline "cic:/CoRN/ftc/FunctSequence/F.var". -inline cic:/CoRN/ftc/FunctSequence/G.var. +inline "cic:/CoRN/ftc/FunctSequence/G.var". -inline cic:/CoRN/ftc/FunctSequence/contF.var. +inline "cic:/CoRN/ftc/FunctSequence/contF.var". -inline cic:/CoRN/ftc/FunctSequence/contG.var. +inline "cic:/CoRN/ftc/FunctSequence/contG.var". (* begin show *) -inline cic:/CoRN/ftc/FunctSequence/convF.var. +inline "cic:/CoRN/ftc/FunctSequence/convF.var". -inline cic:/CoRN/ftc/FunctSequence/convG.var. +inline "cic:/CoRN/ftc/FunctSequence/convG.var". (* end show *) (* begin hide *) -inline cic:/CoRN/ftc/FunctSequence/incf.con. +inline "cic:/CoRN/ftc/FunctSequence/incf.con". -inline cic:/CoRN/ftc/FunctSequence/incg.con. +inline "cic:/CoRN/ftc/FunctSequence/incg.con". -inline cic:/CoRN/ftc/FunctSequence/incF.con. +inline "cic:/CoRN/ftc/FunctSequence/incF.con". -inline cic:/CoRN/ftc/FunctSequence/incG.con. +inline "cic:/CoRN/ftc/FunctSequence/incG.con". (* end hide *) -inline cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_plus'.con. +inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_plus'.con". -inline cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_minus'.con. +inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_minus'.con". -inline cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_mult'.con. +inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_mult'.con". (* UNEXPORTED End Algebraic_Properties. @@ -420,25 +418,25 @@ End Algebraic_Properties. Section More_Algebraic_Properties. *) -inline cic:/CoRN/ftc/FunctSequence/a.var. +inline "cic:/CoRN/ftc/FunctSequence/a.var". -inline cic:/CoRN/ftc/FunctSequence/b.var. +inline "cic:/CoRN/ftc/FunctSequence/b.var". -inline cic:/CoRN/ftc/FunctSequence/Hab.var. +inline "cic:/CoRN/ftc/FunctSequence/Hab.var". (* begin hide *) -inline cic:/CoRN/ftc/FunctSequence/I.con. +inline "cic:/CoRN/ftc/FunctSequence/I.con". (* end hide *) -inline cic:/CoRN/ftc/FunctSequence/f.var. +inline "cic:/CoRN/ftc/FunctSequence/f.var". -inline cic:/CoRN/ftc/FunctSequence/g.var. +inline "cic:/CoRN/ftc/FunctSequence/g.var". -inline cic:/CoRN/ftc/FunctSequence/contf.var. +inline "cic:/CoRN/ftc/FunctSequence/contf.var". -inline cic:/CoRN/ftc/FunctSequence/contg.var. +inline "cic:/CoRN/ftc/FunctSequence/contg.var". (*#* The same is true if we don't make the limits explicit. @@ -446,23 +444,23 @@ The same is true if we don't make the limits explicit. (* begin hide *) -inline cic:/CoRN/ftc/FunctSequence/Hf.var. +inline "cic:/CoRN/ftc/FunctSequence/Hf.var". -inline cic:/CoRN/ftc/FunctSequence/Hg.var. +inline "cic:/CoRN/ftc/FunctSequence/Hg.var". (* end hide *) -inline cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_plus.con. +inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_plus.con". -inline cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_plus.con. +inline "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_plus.con". -inline cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_minus.con. +inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_minus.con". -inline cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_minus.con. +inline "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_minus.con". -inline cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_mult.con. +inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_mult.con". -inline cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_mult.con. +inline "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_mult.con". (* UNEXPORTED End More_Algebraic_Properties. @@ -472,31 +470,31 @@ End More_Algebraic_Properties. Section Still_More_Algebraic_Properties. *) -inline cic:/CoRN/ftc/FunctSequence/a.var. +inline "cic:/CoRN/ftc/FunctSequence/a.var". -inline cic:/CoRN/ftc/FunctSequence/b.var. +inline "cic:/CoRN/ftc/FunctSequence/b.var". -inline cic:/CoRN/ftc/FunctSequence/Hab.var. +inline "cic:/CoRN/ftc/FunctSequence/Hab.var". (* begin hide *) -inline cic:/CoRN/ftc/FunctSequence/I.con. +inline "cic:/CoRN/ftc/FunctSequence/I.con". (* end hide *) -inline cic:/CoRN/ftc/FunctSequence/f.var. +inline "cic:/CoRN/ftc/FunctSequence/f.var". -inline cic:/CoRN/ftc/FunctSequence/contf.var. +inline "cic:/CoRN/ftc/FunctSequence/contf.var". -inline cic:/CoRN/ftc/FunctSequence/Hf.var. +inline "cic:/CoRN/ftc/FunctSequence/Hf.var". (*#* As a corollary, we get the analogous property for the sequence of algebraic inverse functions. *) -inline cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_inv.con. +inline "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_inv.con". -inline cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_inv.con. +inline "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_inv.con". (* UNEXPORTED End Still_More_Algebraic_Properties.