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".
21 include "algebra/COrdAbs.ma".
26 Section OrdField_Cauchy
29 (*#* **Cauchy sequences
30 %\begin{convention}% Let [R] be an ordered field.
34 alias id "R" = "cic:/CoRN/algebra/COrdCauchy/OrdField_Cauchy/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 coercion cic:/matita/CoRN-Decl/algebra/COrdCauchy/CS_seq.con 0 (* compounds *).
75 inline "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 "cic:/CoRN/algebra/COrdCauchy/CS_seq_bounded.con".
91 inline "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 "cic:/CoRN/algebra/COrdCauchy/CS_seq_plus.con".
108 inline "cic:/CoRN/algebra/COrdCauchy/CS_seq_inv.con".
110 inline "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 "cic:/CoRN/algebra/COrdCauchy/CS_seq_recip_def.con".
134 inline "cic:/CoRN/algebra/COrdCauchy/CS_seq_recip_seq.con".
136 inline "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 "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 "cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall'_rht.con".
167 inline "cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall_rht.con".
169 inline "cic:/CoRN/algebra/COrdCauchy/mult_AbsSmall_lft.con".
171 inline "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 "cic:/CoRN/algebra/COrdCauchy/smaller.con".
191 inline "cic:/CoRN/algebra/COrdCauchy/estimate_abs.con".
193 inline "cic:/CoRN/algebra/COrdCauchy/mult_contin.con".
195 (*#* Addition is also continuous. *)
197 inline "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 "cic:/CoRN/algebra/COrdCauchy/resp_less_char'.con".
226 inline "cic:/CoRN/algebra/COrdCauchy/resp_less_char.con".
228 inline "cic:/CoRN/algebra/COrdCauchy/resp_leEq_char'.con".
230 inline "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 "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/local_mon'_imp_mon'.con".
247 inline "cic:/CoRN/algebra/COrdCauchy/mon_imp_mon'.con".
249 inline "cic:/CoRN/algebra/COrdCauchy/mon_imp_inj.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'_lt.con".
257 inline "cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'2_lt.con".
259 inline "cic:/CoRN/algebra/COrdCauchy/mon_imp_mon'_lt.con".
261 inline "cic:/CoRN/algebra/COrdCauchy/mon_imp_inj_lt.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'_le.con".
269 inline "cic:/CoRN/algebra/COrdCauchy/local_mon'_imp_mon'2_le.con".
271 inline "cic:/CoRN/algebra/COrdCauchy/mon_imp_mon'_le.con".
273 inline "cic:/CoRN/algebra/COrdCauchy/mon_imp_inj_le.con".
276 A similar result for %{\em %partial%}% functions.
279 inline "cic:/CoRN/algebra/COrdCauchy/part_mon_imp_mon'.con".
282 End Monotonous_functions