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/".
19 record is_total_order_relation (C:Type) (le:C→C→Prop) : Type \def
20 { to_cotransitive: ∀x,y,z:C. le x y → le x z ∨ le z y;
21 to_antisimmetry: ∀x,y:C. le x y → le y x → x=y
24 theorem to_transitive: ∀C,le. is_total_order_relation C le → transitive ? le.
28 elim (to_cotransitive ? ? i ? ? z H);
30 | rewrite < (to_antisimmetry ? ? i ? ? H1 t);
35 record is_ordered_field_ch0 (F:field) (le:F→F→Prop) : Type \def
36 { of_total_order_relation:> is_total_order_relation ? le;
37 of_mult_compat: ∀a,b. le 0 a → le 0 b → le 0 (a*b);
38 of_plus_compat: ∀a,b,c. le a b → le (a+c) (b+c);
39 of_weak_tricotomy : ∀a,b. a≠b → le a b ∨ le b a;
40 (* 0 characteristics *)
41 of_char0: ∀n. n > O → sum ? (plus F) 0 1 n ≠ 0
44 record ordered_field_ch0 : Type \def
46 of_le: of_field → of_field → Prop;
47 of_ordered_field_properties:> is_ordered_field_ch0 of_field of_le
50 interpretation "Ordered field le" 'leq a b =
51 (cic:/matita/ordered_fields_ch0/of_le.con _ a b).
53 definition lt \def λF:ordered_field_ch0.λa,b:F.a ≤ b ∧ a ≠ b.
55 interpretation "Ordered field lt" 'lt a b =
56 (cic:/matita/ordered_fields_ch0/lt.con _ a b).
58 lemma le_zero_x_to_le_opp_x_zero: ∀F:ordered_field_ch0.∀x:F. 0 ≤ x → -x ≤ 0.
60 generalize in match (of_plus_compat ? ? F ? ? (-x) H); intro;
61 rewrite > zero_neutral in H1;
62 rewrite > plus_comm in H1;
63 rewrite > opp_inverse in H1;
67 lemma le_x_zero_to_le_zero_opp_x: ∀F:ordered_field_ch0.∀x:F. x ≤ 0 → 0 ≤ -x.
69 generalize in match (of_plus_compat ? ? F ? ? (-x) H); intro;
70 rewrite > zero_neutral in H1;
71 rewrite > plus_comm in H1;
72 rewrite > opp_inverse in H1;
77 lemma eq_opp_x_times_opp_one_x: ∀F:ordered_field_ch0.∀x:F.-x = -1*x.
80 lemma not_eq_x_zero_to_lt_zero_mult_x_x:
81 ∀F:ordered_field_ch0.∀x:F. x ≠ 0 → 0 < x * x.
83 elim (of_weak_tricotomy ? ? ? ? ? ? ? ? F ? ? H);
84 [ generalize in match (le_x_zero_to_le_zero_opp_x F ? H1); intro;
85 generalize in match (of_mult_compat ? ? ? ? ? ? ? ? F ? ? H2 H2); intro;
88 axiom lt_zero_to_lt_inv_zero:
89 ∀F:ordered_field_ch0.∀x:F.∀p:x≠0. 0 < x → 0 < inv ? x p.
91 (* The ordering is not necessary. *)
92 axiom not_eq_sum_field_zero: ∀F:ordered_field_ch0.∀n. O<n → sum_field F n ≠ 0.
93 axiom le_zero_sum_field: ∀F:ordered_field_ch0.∀n. O<n → 0 < sum_field F n.
95 axiom lt_zero_to_le_inv_zero:
96 ∀F:ordered_field_ch0.∀n:nat.∀p:sum_field F n ≠ 0. 0 ≤ inv ? (sum_field F n) p.
98 definition tends_to : ∀F:ordered_field_ch0.∀f:nat→F.∀l:F.Prop.
99 alias symbol "leq" = "Ordered field le".
100 alias id "le" = "cic:/matita/nat/orders/le.ind#xpointer(1/1)".
102 (λF:ordered_field_ch0.λf:nat → F.λl:F.
103 ∀n:nat.∃m:nat.∀j:nat. le m j →
104 l - (inv F (sum_field F (S n)) ?) ≤ f j ∧
105 f j ≤ l + (inv F (sum_field F (S n)) ?));
106 apply not_eq_sum_field_zero;
112 definition is_cauchy_seq ≝
113 λF:ordered_field_ch0.λf:nat→F.
116 -eps ≤ f M - f n ∧ f M - f n ≤ eps.
121 definition is_cauchy_seq : ∀F:ordered_field_ch0.∀f:nat→F.Prop.
123 (λF:ordered_field_ch0.λf:nat→F.
126 -(inv ? (sum_field F (S m)) ?) ≤ f N - f n ∧
127 f N - f n ≤ inv ? (sum_field F (S m)) ?);
128 apply not_eq_sum_field_zero;
133 definition is_complete ≝
134 λF:ordered_field_ch0.
135 ∀f:nat→F. is_cauchy_seq ? f →
136 ex F (λl:F. tends_to ? f l).