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/ordered_fields_ch0/".
18 include "ordered_sets.ma".
20 (*CSC: non capisco questi alias! Una volta non servivano*)
21 alias id "plus" = "cic:/matita/groups/plus.con".
22 alias symbol "plus" = "Abelian group plus".
23 record is_ordered_field_ch0 (F:field) (le:F→F→Prop) : Type \def
24 { of_mult_compat: ∀a,b. le 0 a → le 0 b → le 0 (a*b);
25 of_plus_compat: ∀a,b,c. le a b → le (a+c) (b+c);
26 of_weak_tricotomy : ∀a,b. a≠b → le a b ∨ le b a;
27 (* 0 characteristics *)
28 (*CSC: qua c'era un ? al posto di F *)
29 of_char0: ∀n. n > O → sum F (plus F) 0 1 n ≠ 0
32 record ordered_field_ch0 : Type \def
34 of_ordered_set:> ordered_set of_field;
35 of_reflexive: reflexive ? (os_le ? of_ordered_set);
36 of_antisimmetric: antisimmetric ? (os_le ? of_ordered_set);
37 of_cotransitive: cotransitive ? (os_le ? of_ordered_set);
38 (*CSC: qui c'era un ? al posto di of_field *)
39 of_ordered_field_properties:> is_ordered_field_ch0 of_field (os_le ? of_ordered_set)
42 (*theorem ordered_set_of_ordered_field_ch0:
43 ∀F:ordered_field_ch0.ordered_set F.
46 [ apply (mk_pre_ordered_set ? (of_le F))
47 | apply mk_is_order_relation;
48 [ apply (of_reflexive F)
49 | apply antisimmetric_to_cotransitive_to_transitive;
50 [ apply (of_antisimmetric F)
51 | apply (of_cotransitive F)
53 | apply (of_antisimmetric F)
58 coercion cic:/matita/ordered_fields_ch0/ordered_set_of_ordered_field_ch0.con.
61 (*interpretation "Ordered field le" 'leq a b =
62 (cic:/matita/ordered_fields_ch0/of_le.con _ a b).
65 (*CSC: qua c'era uno zero*)
66 lemma le_zero_x_to_le_opp_x_zero: ∀F:ordered_field_ch0.∀x:F.(zero F) ≤ x → -x ≤ 0.
68 generalize in match (of_plus_compat ? ? F ? ? (-x) H); intro;
69 rewrite > zero_neutral in H1;
70 rewrite > plus_comm in H1;
71 rewrite > opp_inverse in H1;
72 (*assumption*)apply H1.
75 (*CSC: qua c'era uno zero*)
76 lemma le_x_zero_to_le_zero_opp_x: ∀F:ordered_field_ch0.∀x:F. x ≤ 0 → (zero F) ≤ -x.
78 generalize in match (of_plus_compat ? ? F ? ? (-x) H); intro;
79 rewrite > zero_neutral in H1;
80 rewrite > plus_comm in H1;
81 rewrite > opp_inverse in H1;
82 (*assumption.*) apply H1.
86 lemma eq_opp_x_times_opp_one_x: ∀F:ordered_field_ch0.∀x:F.-x = -1*x.
89 lemma not_eq_x_zero_to_lt_zero_mult_x_x:
90 ∀F:ordered_field_ch0.∀x:F. x ≠ 0 → 0 < x * x.
92 elim (of_weak_tricotomy ? ? ? ? ? ? ? ? F ? ? H);
93 [ generalize in match (le_x_zero_to_le_zero_opp_x F ? H1); intro;
94 generalize in match (of_mult_compat ? ? ? ? ? ? ? ? F ? ? H2 H2); intro;
97 axiom lt_zero_to_lt_inv_zero:
98 ∀F:ordered_field_ch0.∀x:F.∀p:x≠0. lt ? F 0 x → lt ? F 0 (inv ? x p).
100 alias symbol "lt" = "natural 'less than'".
102 (* The ordering is not necessary. *)
103 axiom not_eq_sum_field_zero: ∀F:ordered_field_ch0.∀n. O<n → sum_field F n ≠ 0.
104 axiom le_zero_sum_field: ∀F:ordered_field_ch0.∀n. O<n → lt ? F 0 (sum_field F n).
106 axiom lt_zero_to_le_inv_zero:
107 ∀F:ordered_field_ch0.∀n:nat.∀p:sum_field F n ≠ 0. os_le ? F 0 (inv ? (sum_field ? n) p).
109 definition tends_to : ∀F:ordered_field_ch0.∀f:nat→F.∀l:F.Prop.
111 (λF:ordered_field_ch0.λf:nat → F.λl:F.
112 ∀n:nat.∃m:nat.∀j:nat. le m j →
113 l - (inv F (sum_field ? (S n)) ?) ≤ f j ∧
114 f j ≤ l + (inv F (sum_field ? (S n)) ?));
115 apply not_eq_sum_field_zero;
121 definition is_cauchy_seq ≝
122 λF:ordered_field_ch0.λf:nat→F.
125 -eps ≤ f M - f n ∧ f M - f n ≤ eps.
130 definition is_cauchy_seq : ∀F:ordered_field_ch0.∀f:nat→F.Prop.
132 (λF:ordered_field_ch0.λf:nat→F.
135 -(inv ? (sum_field F (S m)) ?) ≤ f N - f n ∧
136 f N - f n ≤ inv ? (sum_field F (S m)) ?);
137 apply not_eq_sum_field_zero;
142 definition is_complete ≝
143 λF:ordered_field_ch0.
144 ∀f:nat→F. is_cauchy_seq ? f →
145 ex F (λl:F. tends_to ? f l).