1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (* $Id: CReals1.v,v 1.4 2004/04/23 10:01:04 lcf Exp $ *)
21 include "reals/Max_AbsIR.ma".
23 include "algebra/Expon.ma".
25 include "algebra/CPoly_ApZero.ma".
28 Section More_Cauchy_Props
32 *** More properties of Cauchy sequences
33 We will now define some special Cauchy sequences and prove some
34 more useful properties about them.
36 The sequence defined by $x_n=\frac2{n+1}$#x(n)=2/(n+1)#.
39 inline procedural "cic:/CoRN/reals/CReals1/twice_inv_seq_Lim.con" as lemma.
41 inline procedural "cic:/CoRN/reals/CReals1/twice_inv_seq.con" as definition.
44 Next, we prove that the sequence of absolute values of a Cauchy
45 sequence is also Cauchy.
48 inline procedural "cic:/CoRN/reals/CReals1/Cauchy_Lim_abs.con" as lemma.
50 inline procedural "cic:/CoRN/reals/CReals1/Cauchy_abs.con" as lemma.
52 inline procedural "cic:/CoRN/reals/CReals1/Lim_abs.con" as lemma.
63 We will now examine (although without formalizing it) the concept
64 of subsequence and some of its properties.
66 %\begin{convention}% Let [seq1,seq2:nat->IR].
69 In order for [seq1] to be a subsequence of [seq2], there must be an
70 increasing function [f] growing to infinity such that
71 [forall (n :nat), (seq1 n) [=] (seq2 (f n))]. We assume [f] to be such a
74 Finally, for some of our results it is important to assume that
79 cic:/CoRN/reals/CReals1/Subsequences/seq1.var
83 cic:/CoRN/reals/CReals1/Subsequences/seq2.var
87 cic:/CoRN/reals/CReals1/Subsequences/f.var
91 cic:/CoRN/reals/CReals1/Subsequences/monF.var
95 cic:/CoRN/reals/CReals1/Subsequences/crescF.var
99 cic:/CoRN/reals/CReals1/Subsequences/subseq.var
103 cic:/CoRN/reals/CReals1/Subsequences/mon_seq2.var
106 inline procedural "cic:/CoRN/reals/CReals1/unbnd_f.con" as lemma.
110 inline procedural "cic:/CoRN/reals/CReals1/Subsequences/mon_F'.con" "Subsequences__" as definition.
114 inline procedural "cic:/CoRN/reals/CReals1/conv_subseq_imp_conv_seq.con" as lemma.
116 inline procedural "cic:/CoRN/reals/CReals1/Cprop2_seq_imp_Cprop2_subseq.con" as lemma.
118 inline procedural "cic:/CoRN/reals/CReals1/conv_seq_imp_conv_subseq.con" as lemma.
120 inline procedural "cic:/CoRN/reals/CReals1/Cprop2_subseq_imp_Cprop2_seq.con" as lemma.
127 Section Cauchy_Subsequences
131 cic:/CoRN/reals/CReals1/Cauchy_Subsequences/seq1.var
135 cic:/CoRN/reals/CReals1/Cauchy_Subsequences/seq2.var
139 cic:/CoRN/reals/CReals1/Cauchy_Subsequences/f.var
143 cic:/CoRN/reals/CReals1/Cauchy_Subsequences/monF.var
147 cic:/CoRN/reals/CReals1/Cauchy_Subsequences/crescF.var
151 cic:/CoRN/reals/CReals1/Cauchy_Subsequences/subseq.var
155 cic:/CoRN/reals/CReals1/Cauchy_Subsequences/mon_seq2.var
158 inline procedural "cic:/CoRN/reals/CReals1/Lim_seq_eq_Lim_subseq.con" as lemma.
160 inline procedural "cic:/CoRN/reals/CReals1/Lim_subseq_eq_Lim_seq.con" as lemma.
163 End Cauchy_Subsequences
167 Section Properties_of_Exponentiation
170 (*#* *** More properties of Exponentiation
172 Finally, we prove that [x[^]n] grows to infinity if [x [>] One].
175 inline procedural "cic:/CoRN/reals/CReals1/power_big'.con" as lemma.
177 inline procedural "cic:/CoRN/reals/CReals1/power_big.con" as lemma.
179 inline procedural "cic:/CoRN/reals/CReals1/qi_yields_zero.con" as lemma.
181 inline procedural "cic:/CoRN/reals/CReals1/qi_lim_zero.con" as lemma.
184 End Properties_of_Exponentiation
187 (*#* *** [IR] has characteristic zero *)
189 inline procedural "cic:/CoRN/reals/CReals1/char0_IR.con" as lemma.
191 inline procedural "cic:/CoRN/reals/CReals1/poly_apzero_IR.con" as lemma.
193 inline procedural "cic:/CoRN/reals/CReals1/poly_IR_extensional.con" as lemma.