(*#* ** [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
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
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
(*#* *** 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
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