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 *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/reals/CReals1".
21 (* $Id: CReals1.v,v 1.4 2004/04/23 10:01:04 lcf Exp $ *)
23 include "reals/Max_AbsIR.ma".
25 include "algebra/Expon.ma".
27 include "algebra/CPoly_ApZero.ma".
30 Section More_Cauchy_Props.
34 *** More properties of Cauchy sequences
35 We will now define some special Cauchy sequences and prove some
36 more useful properties about them.
38 The sequence defined by $x_n=\frac2{n+1}$#x(n)=2/(n+1)#.
41 inline "cic:/CoRN/reals/CReals1/twice_inv_seq_Lim.con".
43 inline "cic:/CoRN/reals/CReals1/twice_inv_seq.con".
46 Next, we prove that the sequence of absolute values of a Cauchy
47 sequence is also Cauchy.
50 inline "cic:/CoRN/reals/CReals1/Cauchy_Lim_abs.con".
52 inline "cic:/CoRN/reals/CReals1/Cauchy_abs.con".
54 inline "cic:/CoRN/reals/CReals1/Lim_abs.con".
57 End More_Cauchy_Props.
65 We will now examine (although without formalizing it) the concept
66 of subsequence and some of its properties.
68 %\begin{convention}% Let [seq1,seq2:nat->IR].
71 In order for [seq1] to be a subsequence of [seq2], there must be an
72 increasing function [f] growing to infinity such that
73 [forall (n :nat), (seq1 n) [=] (seq2 (f n))]. We assume [f] to be such a
76 Finally, for some of our results it is important to assume that
80 inline "cic:/CoRN/reals/CReals1/seq1.var".
82 inline "cic:/CoRN/reals/CReals1/seq2.var".
84 inline "cic:/CoRN/reals/CReals1/f.var".
86 inline "cic:/CoRN/reals/CReals1/monF.var".
88 inline "cic:/CoRN/reals/CReals1/crescF.var".
90 inline "cic:/CoRN/reals/CReals1/subseq.var".
92 inline "cic:/CoRN/reals/CReals1/mon_seq2.var".
94 inline "cic:/CoRN/reals/CReals1/unbnd_f.con".
98 inline "cic:/CoRN/reals/CReals1/mon_F'.con".
102 inline "cic:/CoRN/reals/CReals1/conv_subseq_imp_conv_seq.con".
104 inline "cic:/CoRN/reals/CReals1/Cprop2_seq_imp_Cprop2_subseq.con".
106 inline "cic:/CoRN/reals/CReals1/conv_seq_imp_conv_subseq.con".
108 inline "cic:/CoRN/reals/CReals1/Cprop2_subseq_imp_Cprop2_seq.con".
115 Section Cauchy_Subsequences.
118 inline "cic:/CoRN/reals/CReals1/seq1.var".
120 inline "cic:/CoRN/reals/CReals1/seq2.var".
122 inline "cic:/CoRN/reals/CReals1/f.var".
124 inline "cic:/CoRN/reals/CReals1/monF.var".
126 inline "cic:/CoRN/reals/CReals1/crescF.var".
128 inline "cic:/CoRN/reals/CReals1/subseq.var".
130 inline "cic:/CoRN/reals/CReals1/mon_seq2.var".
132 inline "cic:/CoRN/reals/CReals1/Lim_seq_eq_Lim_subseq.con".
134 inline "cic:/CoRN/reals/CReals1/Lim_subseq_eq_Lim_seq.con".
137 End Cauchy_Subsequences.
141 Section Properties_of_Exponentiation.
144 (*#* *** More properties of Exponentiation
146 Finally, we prove that [x[^]n] grows to infinity if [x [>] One].
149 inline "cic:/CoRN/reals/CReals1/power_big'.con".
151 inline "cic:/CoRN/reals/CReals1/power_big.con".
153 inline "cic:/CoRN/reals/CReals1/qi_yields_zero.con".
155 inline "cic:/CoRN/reals/CReals1/qi_lim_zero.con".
158 End Properties_of_Exponentiation.
161 (*#* *** [IR] has characteristic zero *)
163 inline "cic:/CoRN/reals/CReals1/char0_IR.con".
165 inline "cic:/CoRN/reals/CReals1/poly_apzero_IR.con".
167 inline "cic:/CoRN/reals/CReals1/poly_IR_extensional.con".