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/algebra/COrdCauchy".
26 Section OrdField_Cauchy.
29 (*#* **Cauchy sequences
30 %\begin{convention}% Let [R] be an ordered field.
34 inline cic:/CoRN/algebra/COrdCauchy/R.var.
39 Set Implicit Arguments.
43 Unset Strict Implicit.
48 inline cic:/CoRN/algebra/COrdCauchy/Cauchy_prop.con.
57 Unset Implicit Arguments.
62 (* Def. CauchyP, Build_CauchyP *)
64 (* Should be defined in terms of CauchyP *)
67 Implicit arguments turned off, because Coq makes a mess of it in combination
71 inline cic:/CoRN/algebra/COrdCauchy/CauchySeq.ind.
73 inline cic:/CoRN/algebra/COrdCauchy/SeqLimit.con.
78 We now prove that the property of being a Cauchy sequence is preserved
79 through the usual algebraic operations (addition, subtraction and
80 multiplication -- and division, provided some additional conditions
83 %\begin{convention}% Let [R] be an ordered field.
87 inline cic:/CoRN/algebra/COrdCauchy/CS_seq_bounded.con.
89 inline cic:/CoRN/algebra/COrdCauchy/CS_seq_const.con.
92 %\begin{convention}% Assume [f] and [g] are Cauchy sequences on [R].
96 inline cic:/CoRN/algebra/COrdCauchy/f.var.
98 inline cic:/CoRN/algebra/COrdCauchy/g.var.
100 inline cic:/CoRN/algebra/COrdCauchy/Hf.var.
102 inline cic:/CoRN/algebra/COrdCauchy/Hg.var.
104 inline cic:/CoRN/algebra/COrdCauchy/CS_seq_plus.con.
106 inline cic:/CoRN/algebra/COrdCauchy/CS_seq_inv.con.
108 inline cic:/CoRN/algebra/COrdCauchy/CS_seq_mult.con.
111 We now assume that [f] is, from some point onwards, greater than
112 some positive number. The sequence of reciprocals is defined as
113 being constantly one up to that point, and the sequence of
114 reciprocals from then onwards.
117 Let [e] be a postive element of [R] and let [N:nat] be such that from
118 [N] onwards, [(f n) [#] Zero]
122 inline cic:/CoRN/algebra/COrdCauchy/e.var.
124 inline cic:/CoRN/algebra/COrdCauchy/He.var.
126 inline cic:/CoRN/algebra/COrdCauchy/N.var.
128 inline cic:/CoRN/algebra/COrdCauchy/f_bnd.var.
130 inline cic:/CoRN/algebra/COrdCauchy/CS_seq_recip_def.con.
132 inline cic:/CoRN/algebra/COrdCauchy/CS_seq_recip_seq.con.
134 inline cic:/CoRN/algebra/COrdCauchy/CS_seq_recip.con.
141 Implicit Arguments SeqLimit [R].
145 The following lemma does not require the sequence to be Cauchy, but it fits
149 inline cic:/CoRN/algebra/COrdCauchy/maj_upto_eps.con.
152 Section Mult_AbsSmall.
155 inline cic:/CoRN/algebra/COrdCauchy/R.var.
158 ** [AbsSmall] revisited
159 %\begin{convention}% Let [R] be an ordered field.
163 inline cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall'_rht.con.
165 inline cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall_rht.con.
167 inline cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall_lft.con.
169 inline cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall.con.
176 Section Mult_Continuous.
179 inline cic:/CoRN/algebra/COrdCauchy/R.var.
182 ** Multiplication is continuous
183 %\begin{convention}% Let [R] be an ordered field.
187 inline cic:/CoRN/algebra/COrdCauchy/smaller.con.
189 inline cic:/CoRN/algebra/COrdCauchy/estimate_abs.con.
191 inline cic:/CoRN/algebra/COrdCauchy/mult_contin.con.
193 (*#* Addition is also continuous. *)
195 inline cic:/CoRN/algebra/COrdCauchy/plus_contin.con.
202 Section Monotonous_functions.
206 ** Monotonous Functions
208 Finally, we study several properties of monotonous functions and
209 characterize them in some way.
211 %\begin{convention}% Let [R] be an ordered field.
215 inline cic:/CoRN/algebra/COrdCauchy/R.var.
218 We begin by characterizing the preservation of less (less or equal)
219 in terms of preservation of less or equal (less).
222 inline cic:/CoRN/algebra/COrdCauchy/resp_less_char'.con.
224 inline cic:/CoRN/algebra/COrdCauchy/resp_less_char.con.
226 inline cic:/CoRN/algebra/COrdCauchy/resp_leEq_char'.con.
228 inline cic:/CoRN/algebra/COrdCauchy/resp_leEq_char.con.
231 Next, we see different characterizations of monotonous functions from
232 some subset of the natural numbers into [R]. Mainly, these
233 amount (for different types of functions) to proving that a function
234 is monotonous iff [f(i) [<] f(i+1)] for every [i].
236 Also, strictly monotonous functions are injective.
239 inline cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon.con.
241 inline cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon'.con.
243 inline cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'.con.
245 inline cic:/CoRN/algebra/COrdCauchy/mon_imp_mon'.con.
247 inline cic:/CoRN/algebra/COrdCauchy/mon_imp_inj.con.
249 inline cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon_lt.con.
251 inline cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon'_lt.con.
253 inline cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'_lt.con.
255 inline cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'2_lt.con.
257 inline cic:/CoRN/algebra/COrdCauchy/mon_imp_mon'_lt.con.
259 inline cic:/CoRN/algebra/COrdCauchy/mon_imp_inj_lt.con.
261 inline cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon_le.con.
263 inline cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon'_le.con.
265 inline cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'_le.con.
267 inline cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'2_le.con.
269 inline cic:/CoRN/algebra/COrdCauchy/mon_imp_mon'_le.con.
271 inline cic:/CoRN/algebra/COrdCauchy/mon_imp_inj_le.con.
274 A similar result for %{\em %partial%}% functions.
277 inline cic:/CoRN/algebra/COrdCauchy/part_mon_imp_mon'.con.
280 End Monotonous_functions.