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 set "baseuri" "cic:/matita/reals/".
17 include "ordered_fields_ch0.ma".
19 record is_real (F:ordered_field_ch0) : Prop
21 { r_archimedean: ∀x:F. ∃n:nat. x ≤ (sum_field F n);
22 r_complete: is_complete F
25 record real: Type \def
26 { r_ordered_field_ch0:> ordered_field_ch0;
27 r_real_properties: is_real r_ordered_field_ch0
30 (* serve l'esistenziale in CProp!
31 definition lim: ∀R:real.∀f:nat→R.is_cauchy_seq R f → R.
37 definition max_seq: ∀R:real.∀x,y:R. nat → R.
39 elim (to_cotransitive R (of_le R) R 0 (inv ? (sum_field R (S n)) ?) (x-y));
41 | apply not_eq_sum_field_zero ;
45 | apply lt_zero_to_le_inv_zero
49 theorem cauchy_max_seq: ∀R:real.∀x,y. is_cauchy_seq ? (max_seq R x y).
53 apply (ex_intro ? ? m);
58 elim (to_cotransitive R (of_le R) R 0
59 (inv R (sum_field R (S N))
60 (not_eq_sum_field_zero R (S N) (le_S_S O N (le_O_n N)))) (x-y)
61 (lt_zero_to_le_inv_zero R (S N)
62 (not_eq_sum_field_zero R (S N) (le_S_S O N (le_O_n N)))));
64 elim (to_cotransitive R (of_le R) R 0
65 (inv R (1+sum R (plus R) 0 1 m)
66 (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))) (x-y)
67 (lt_zero_to_le_inv_zero R (S m)
68 (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))));
70 rewrite > (plus_comm ? x (-x));
71 rewrite > opp_inverse;
72 apply lt_zero_to_le_inv_zero
76 | elim (to_cotransitive R (of_le R) R 0
77 (inv R (1+sum R (plus R) 0 1 m)
78 (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))) (x-y)
79 (lt_zero_to_le_inv_zero R (S m)
80 (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))));
82 generalize in match (le_zero_x_to_le_opp_x_zero R ? t1);
86 rewrite > (plus_comm ? y (-y));
87 rewrite > opp_inverse;
88 apply lt_zero_to_le_inv_zero