matita/contribs/CoRN-Decl/reals/CReals1.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/CoRN-Decl/reals/CReals1".
  18
  19 (* $Id: CReals1.v,v 1.4 2004/04/23 10:01:04 lcf Exp $ *)
  20
  21 (* INCLUDE
  22 Max_AbsIR
  23 *)
  24
  25 (* INCLUDE
  26 Expon
  27 *)
  28
  29 (* INCLUDE
  30 CPoly_ApZero
  31 *)
  32
  33 (* UNEXPORTED
  34 Section More_Cauchy_Props.
  35 *)
  36
  37 (*#* **Miscellaneous
  38 *** More properties of Cauchy sequences
  39 We will now define some special Cauchy sequences and prove some
  40 more useful properties about them.
  41
  42 The sequence defined by $x_n=\frac2{n+1}$#x(n)=2/(n+1)#.
  43 *)
  44
  45 inline cic:/CoRN/reals/CReals1/twice_inv_seq_Lim.con.
  46
  47 inline cic:/CoRN/reals/CReals1/twice_inv_seq.con.
  48
  49 (*#*
  50 Next, we prove that the sequence of absolute values of a Cauchy
  51 sequence is also Cauchy.
  52 *)
  53
  54 inline cic:/CoRN/reals/CReals1/Cauchy_Lim_abs.con.
  55
  56 inline cic:/CoRN/reals/CReals1/Cauchy_abs.con.
  57
  58 inline cic:/CoRN/reals/CReals1/Lim_abs.con.
  59
  60 (* UNEXPORTED
  61 End More_Cauchy_Props.
  62 *)
  63
  64 (* UNEXPORTED
  65 Section Subsequences.
  66 *)
  67
  68 (*#* *** Subsequences
  69 We will now examine (although without formalizing it) the concept
  70 of subsequence and some of its properties.
  71
  72 %\begin{convention}% Let [seq1,seq2:nat->IR].
  73 %\end{convention}%
  74
  75 In order for [seq1] to be a subsequence of [seq2], there must be an
  76 increasing function [f] growing to infinity such that
  77 [forall (n :nat), (seq1 n) [=] (seq2 (f n))].  We assume [f] to be such a
  78 function.
  79
  80 Finally, for some of our results it is important to assume that
  81 [seq2] is monotonous.
  82 *)
  83
  84 inline cic:/CoRN/reals/CReals1/seq1.var.
  85
  86 inline cic:/CoRN/reals/CReals1/seq2.var.
  87
  88 inline cic:/CoRN/reals/CReals1/f.var.
  89
  90 inline cic:/CoRN/reals/CReals1/monF.var.
  91
  92 inline cic:/CoRN/reals/CReals1/crescF.var.
  93
  94 inline cic:/CoRN/reals/CReals1/subseq.var.
  95
  96 inline cic:/CoRN/reals/CReals1/mon_seq2.var.
  97
  98 inline cic:/CoRN/reals/CReals1/unbnd_f.con.
  99
 100 (* begin hide *)
 101
 102 inline cic:/CoRN/reals/CReals1/mon_F'.con.
 103
 104 (* end hide *)
 105
 106 inline cic:/CoRN/reals/CReals1/conv_subseq_imp_conv_seq.con.
 107
 108 inline cic:/CoRN/reals/CReals1/Cprop2_seq_imp_Cprop2_subseq.con.
 109
 110 inline cic:/CoRN/reals/CReals1/conv_seq_imp_conv_subseq.con.
 111
 112 inline cic:/CoRN/reals/CReals1/Cprop2_subseq_imp_Cprop2_seq.con.
 113
 114 (* UNEXPORTED
 115 End Subsequences.
 116 *)
 117
 118 (* UNEXPORTED
 119 Section Cauchy_Subsequences.
 120 *)
 121
 122 inline cic:/CoRN/reals/CReals1/seq1.var.
 123
 124 inline cic:/CoRN/reals/CReals1/seq2.var.
 125
 126 inline cic:/CoRN/reals/CReals1/f.var.
 127
 128 inline cic:/CoRN/reals/CReals1/monF.var.
 129
 130 inline cic:/CoRN/reals/CReals1/crescF.var.
 131
 132 inline cic:/CoRN/reals/CReals1/subseq.var.
 133
 134 inline cic:/CoRN/reals/CReals1/mon_seq2.var.
 135
 136 inline cic:/CoRN/reals/CReals1/Lim_seq_eq_Lim_subseq.con.
 137
 138 inline cic:/CoRN/reals/CReals1/Lim_subseq_eq_Lim_seq.con.
 139
 140 (* UNEXPORTED
 141 End Cauchy_Subsequences.
 142 *)
 143
 144 (* UNEXPORTED
 145 Section Properties_of_Exponentiation.
 146 *)
 147
 148 (*#* *** More properties of Exponentiation
 149
 150 Finally, we prove that [x[^]n] grows to infinity if [x [>] One].
 151 *)
 152
 153 inline cic:/CoRN/reals/CReals1/power_big'.con.
 154
 155 inline cic:/CoRN/reals/CReals1/power_big.con.
 156
 157 inline cic:/CoRN/reals/CReals1/qi_yields_zero.con.
 158
 159 inline cic:/CoRN/reals/CReals1/qi_lim_zero.con.
 160
 161 (* UNEXPORTED
 162 End Properties_of_Exponentiation.
 163 *)
 164
 165 (*#* *** [IR] has characteristic zero *)
 166
 167 inline cic:/CoRN/reals/CReals1/char0_IR.con.
 168
 169 inline cic:/CoRN/reals/CReals1/poly_apzero_IR.con.
 170
 171 inline cic:/CoRN/reals/CReals1/poly_IR_extensional.con.
 172