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 include "algebra/COrdAbs.ma".
24 Section OrdField_Cauchy
27 (*#* **Cauchy sequences
28 %\begin{convention}% Let [R] be an ordered field.
32 alias id "R" = "cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/R.var".
37 Set Implicit Arguments.
41 Unset Strict Implicit.
46 inline procedural "cic:/CoRN/algebra/COrdCauchy/Cauchy_prop.con".
55 Unset Implicit Arguments.
60 (* Def. CauchyP, Build_CauchyP *)
62 (* Should be defined in terms of CauchyP *)
65 Implicit arguments turned off, because Coq makes a mess of it in combination
69 inline procedural "cic:/CoRN/algebra/COrdCauchy/CauchySeq.ind".
72 cic:/matita/CoRN-Procedural/algebra/COrdCauchy/CS_seq.con
75 inline procedural "cic:/CoRN/algebra/COrdCauchy/SeqLimit.con".
80 We now prove that the property of being a Cauchy sequence is preserved
81 through the usual algebraic operations (addition, subtraction and
82 multiplication -- and division, provided some additional conditions
85 %\begin{convention}% Let [R] be an ordered field.
89 inline procedural "cic:/CoRN/algebra/COrdCauchy/CS_seq_bounded.con".
91 inline procedural "cic:/CoRN/algebra/COrdCauchy/CS_seq_const.con".
94 %\begin{convention}% Assume [f] and [g] are Cauchy sequences on [R].
98 alias id "f" = "cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/f.var".
100 alias id "g" = "cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/g.var".
102 alias id "Hf" = "cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/Hf.var".
104 alias id "Hg" = "cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/Hg.var".
106 inline procedural "cic:/CoRN/algebra/COrdCauchy/CS_seq_plus.con".
108 inline procedural "cic:/CoRN/algebra/COrdCauchy/CS_seq_inv.con".
110 inline procedural "cic:/CoRN/algebra/COrdCauchy/CS_seq_mult.con".
113 We now assume that [f] is, from some point onwards, greater than
114 some positive number. The sequence of reciprocals is defined as
115 being constantly one up to that point, and the sequence of
116 reciprocals from then onwards.
119 Let [e] be a postive element of [R] and let [N:nat] be such that from
120 [N] onwards, [(f n) [#] Zero]
124 alias id "e" = "cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/e.var".
126 alias id "He" = "cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/He.var".
128 alias id "N" = "cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/N.var".
130 alias id "f_bnd" = "cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/f_bnd.var".
132 inline procedural "cic:/CoRN/algebra/COrdCauchy/CS_seq_recip_def.con".
134 inline procedural "cic:/CoRN/algebra/COrdCauchy/CS_seq_recip_seq.con".
136 inline procedural "cic:/CoRN/algebra/COrdCauchy/CS_seq_recip.con".
143 Implicit Arguments SeqLimit [R].
147 The following lemma does not require the sequence to be Cauchy, but it fits
151 inline procedural "cic:/CoRN/algebra/COrdCauchy/maj_upto_eps.con".
154 Section Mult_AbsSmall
157 alias id "R" = "cic:/CoRN/algebra/COrdCauchy/Mult_AbsSmall/R.var".
160 ** [AbsSmall] revisited
161 %\begin{convention}% Let [R] be an ordered field.
165 inline procedural "cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall'_rht.con".
167 inline procedural "cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall_rht.con".
169 inline procedural "cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall_lft.con".
171 inline procedural "cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall.con".
178 Section Mult_Continuous
181 alias id "R" = "cic:/CoRN/algebra/COrdCauchy/Mult_Continuous/R.var".
184 ** Multiplication is continuous
185 %\begin{convention}% Let [R] be an ordered field.
189 inline procedural "cic:/CoRN/algebra/COrdCauchy/smaller.con".
191 inline procedural "cic:/CoRN/algebra/COrdCauchy/estimate_abs.con".
193 inline procedural "cic:/CoRN/algebra/COrdCauchy/mult_contin.con".
195 (*#* Addition is also continuous. *)
197 inline procedural "cic:/CoRN/algebra/COrdCauchy/plus_contin.con".
204 Section Monotonous_functions
208 ** Monotonous Functions
210 Finally, we study several properties of monotonous functions and
211 characterize them in some way.
213 %\begin{convention}% Let [R] be an ordered field.
217 alias id "R" = "cic:/CoRN/algebra/COrdCauchy/Monotonous_functions/R.var".
220 We begin by characterizing the preservation of less (less or equal)
221 in terms of preservation of less or equal (less).
224 inline procedural "cic:/CoRN/algebra/COrdCauchy/resp_less_char'.con".
226 inline procedural "cic:/CoRN/algebra/COrdCauchy/resp_less_char.con".
228 inline procedural "cic:/CoRN/algebra/COrdCauchy/resp_leEq_char'.con".
230 inline procedural "cic:/CoRN/algebra/COrdCauchy/resp_leEq_char.con".
233 Next, we see different characterizations of monotonous functions from
234 some subset of the natural numbers into [R]. Mainly, these
235 amount (for different types of functions) to proving that a function
236 is monotonous iff [f(i) [<] f(i+1)] for every [i].
238 Also, strictly monotonous functions are injective.
241 inline procedural "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon.con".
243 inline procedural "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon'.con".
245 inline procedural "cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'.con".
247 inline procedural "cic:/CoRN/algebra/COrdCauchy/mon_imp_mon'.con".
249 inline procedural "cic:/CoRN/algebra/COrdCauchy/mon_imp_inj.con".
251 inline procedural "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon_lt.con".
253 inline procedural "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon'_lt.con".
255 inline procedural "cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'_lt.con".
257 inline procedural "cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'2_lt.con".
259 inline procedural "cic:/CoRN/algebra/COrdCauchy/mon_imp_mon'_lt.con".
261 inline procedural "cic:/CoRN/algebra/COrdCauchy/mon_imp_inj_lt.con".
263 inline procedural "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon_le.con".
265 inline procedural "cic:/CoRN/algebra/COrdCauchy/local_mon_imp_mon'_le.con".
267 inline procedural "cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'_le.con".
269 inline procedural "cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'2_le.con".
271 inline procedural "cic:/CoRN/algebra/COrdCauchy/mon_imp_mon'_le.con".
273 inline procedural "cic:/CoRN/algebra/COrdCauchy/mon_imp_inj_le.con".
276 A similar result for %{\em %partial%}% functions.
279 inline procedural "cic:/CoRN/algebra/COrdCauchy/part_mon_imp_mon'.con".
282 End Monotonous_functions