X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Procedural%2Freals%2FCauchySeq.mma;h=16e97d931147c8492bbbf48421843c0aa88c285e;hb=a89360d64f1fcbba917ad743b97a2d973ecf6db2;hp=f6dbff62d53c2187f8f63bc2db304ef8d7d8f14a;hpb=32e77480c65cbf23ae7dea38a519c83dfeaf3830;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Procedural/reals/CauchySeq.mma b/helm/software/matita/contribs/CoRN-Procedural/reals/CauchySeq.mma index f6dbff62d..16e97d931 100644 --- a/helm/software/matita/contribs/CoRN-Procedural/reals/CauchySeq.mma +++ b/helm/software/matita/contribs/CoRN-Procedural/reals/CauchySeq.mma @@ -75,21 +75,21 @@ Section CReals_axioms (*#* ** [CReals] axioms *) -inline procedural "cic:/CoRN/reals/CauchySeq/CReals_is_CReals.con". +inline procedural "cic:/CoRN/reals/CauchySeq/CReals_is_CReals.con" as lemma. (*#* First properties which follow trivially from the axioms. *) -inline procedural "cic:/CoRN/reals/CauchySeq/Lim_Cauchy.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Lim_Cauchy.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Archimedes.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Archimedes.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Archimedes'.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Archimedes'.con" as lemma. (*#* A stronger version, which often comes in useful. *) -inline procedural "cic:/CoRN/reals/CauchySeq/str_Archimedes.con". +inline procedural "cic:/CoRN/reals/CauchySeq/str_Archimedes.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/CauchySeqR.con". +inline procedural "cic:/CoRN/reals/CauchySeq/CauchySeqR.con" as definition. (* UNEXPORTED End CReals_axioms @@ -152,19 +152,19 @@ and [[<=]] being a negative statement, this makes proofs sometimes easier and program extraction much more efficient. *) -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop1.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop1.con" as definition. -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop2.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop2.con" as definition. -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop2.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop2.con" as definition. -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop3.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop3.con" as definition. -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop3.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop3.con" as definition. -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4.con" as definition. -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop4.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop4.con" as definition. (* UNEXPORTED End Cauchy_Defs @@ -178,39 +178,39 @@ Section Inequalities The next lemma is equal to lemma [Lim_Cauchy]. *) -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_complete.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_complete.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/less_Lim_so_less_seq.con". +inline procedural "cic:/CoRN/reals/CauchySeq/less_Lim_so_less_seq.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Lim_less_so_seq_less.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Lim_less_so_seq_less.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Lim_less_Lim_so_seq_less_seq.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Lim_less_Lim_so_seq_less_seq.con" as lemma. (*#* The next lemma follows from [less_Lim_so_less_seq] with [y := (y[+] (Lim seq)) [/]TwoNZ]. *) -inline procedural "cic:/CoRN/reals/CauchySeq/less_Lim_so.con". +inline procedural "cic:/CoRN/reals/CauchySeq/less_Lim_so.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Lim_less_so.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Lim_less_so.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/leEq_seq_so_leEq_Lim.con". +inline procedural "cic:/CoRN/reals/CauchySeq/leEq_seq_so_leEq_Lim.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/str_leEq_seq_so_leEq_Lim.con". +inline procedural "cic:/CoRN/reals/CauchySeq/str_leEq_seq_so_leEq_Lim.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Lim_leEq_Lim.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Lim_leEq_Lim.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/seq_leEq_so_Lim_leEq.con". +inline procedural "cic:/CoRN/reals/CauchySeq/seq_leEq_so_Lim_leEq.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/str_seq_leEq_so_Lim_leEq.con". +inline procedural "cic:/CoRN/reals/CauchySeq/str_seq_leEq_so_Lim_leEq.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Limits_unique.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Limits_unique.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Lim_wd.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Lim_wd.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Lim_strext.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Lim_strext.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Lim_ap_imp_seq_ap.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Lim_ap_imp_seq_ap.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Lim_ap_imp_seq_ap'.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Lim_ap_imp_seq_ap'.con" as lemma. (* UNEXPORTED End Inequalities @@ -222,47 +222,47 @@ Section Equiv_Cauchy (*#* *** Equivalence of formulations of Cauchy *) -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop1_prop.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop1_prop.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop2_prop.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop2_prop.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop3_prop2.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop3_prop2.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop3_prop2.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop3_prop2.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop3_prop.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop3_prop.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq1.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq1.con" as definition. -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4_prop3.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4_prop3.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4_prop2.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4_prop2.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop4_prop3.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop4_prop3.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop4_prop.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop4_prop.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq4.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq4.con" as definition. -inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq4_y.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq4_y.con" as definition. -inline procedural "cic:/CoRN/reals/CauchySeq/Lim_CauchySeq4.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Lim_CauchySeq4.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq2.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq2.con" as definition. -inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq2_y.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq2_y.con" as definition. -inline procedural "cic:/CoRN/reals/CauchySeq/Lim_CauchySeq2.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Lim_CauchySeq2.con" as lemma. (*#* Well definedness. *) -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop_wd.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop_wd.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop2_wd.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop2_wd.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Lim_wd'.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Lim_wd'.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Lim_unique.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Lim_unique.con" as lemma. (* UNEXPORTED End Equiv_Cauchy @@ -279,33 +279,33 @@ Some of these lemmas are now obsolete, because they were reproved for arbitrary We begin by defining the constant sequence and proving that it is Cauchy with the expected limit. *) -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_const.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_const.con" as definition. -inline procedural "cic:/CoRN/reals/CauchySeq/Lim_const.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Lim_const.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_plus.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_plus.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_plus.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_plus.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Lim_plus.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Lim_plus.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_inv.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_inv.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_inv.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_inv.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Lim_inv.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Lim_inv.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_minus.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_minus.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_minus.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_minus.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Lim_minus.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Lim_minus.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_mult.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_mult.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_mult.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_mult.con" as lemma. -inline procedural "cic:/CoRN/reals/CauchySeq/Lim_mult.con". +inline procedural "cic:/CoRN/reals/CauchySeq/Lim_mult.con" as lemma. (* UNEXPORTED End Cauchy_props