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/sequence/".
17 include "excedence.ma".
19 definition sequence := λO:excedence.nat → O.
21 definition fun_of_sequence: ∀O:excedence.sequence O → nat → O.
22 intros; apply s; assumption;
25 coercion cic:/matita/sequence/fun_of_sequence.con 1.
27 definition upper_bound ≝
28 λO:excedence.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
30 definition lower_bound ≝
31 λO:excedence.λa:sequence O.λu:O.∀n:nat.u ≤ a n.
33 definition strong_sup ≝
34 λO:excedence.λs:sequence O.λx.
35 upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y).
37 definition strong_inf ≝
38 λO:excedence.λs:sequence O.λx.
39 lower_bound ? s x ∧ (∀y:O.y ≰ x → ∃n.y ≰ s n).
42 λO:excedence.λs:sequence O.λx.
43 upper_bound ? s x ∧ (∀y:O.upper_bound ? s y → x ≤ y).
46 λO:excedence.λs:sequence O.λx.
47 lower_bound ? s x ∧ (∀y:O.lower_bound ? s y → y ≤ x).
49 lemma strong_sup_is_weak:
50 ∀O:excedence.∀s:sequence O.∀x:O.strong_sup ? s x → weak_sup ? s x.
51 intros (O s x Ssup); elim Ssup (Ubx M); clear Ssup; split; [assumption]
52 intros 3 (y Uby E); cases (M ? E) (n En); unfold in Uby; cases (Uby ? En);
55 lemma strong_inf_is_weak:
56 ∀O:excedence.∀s:sequence O.∀x:O.strong_inf ? s x → weak_inf ? s x.
57 intros (O s x Ssup); elim Ssup (Ubx M); clear Ssup; split; [assumption]
58 intros 3 (y Uby E); cases (M ? E) (n En); unfold in Uby; cases (Uby ? En);
61 include "ordered_group.ma".
62 include "nat/orders.ma".
65 λO:pogroup.λs:sequence O.
66 ∀e:O.0 < e → ∃N.∀n.N < n → -e < s n ∧ s n < e.
68 definition increasing ≝
69 λO:excedence.λa:sequence O.∀n:nat.a n ≤ a (S n).
71 definition decreasing ≝
72 λO:excedence.λa:sequence O.∀n:nat.a (S n) ≤ a n.
79 definition is_upper_bound ≝ λO:excedence.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
80 definition is_lower_bound ≝ λO:excedence.λa:sequence O.λu:O.∀n:nat.u ≤ a n.
82 record is_sup (O:excedence) (a:sequence O) (u:O) : Prop ≝
83 { sup_upper_bound: is_upper_bound O a u;
84 sup_least_upper_bound: ∀v:O. is_upper_bound O a v → u≤v
87 record is_inf (O:excedence) (a:sequence O) (u:O) : Prop ≝
88 { inf_lower_bound: is_lower_bound O a u;
89 inf_greatest_lower_bound: ∀v:O. is_lower_bound O a v → v≤u
92 record is_bounded_below (O:excedence) (a:sequence O) : Type ≝
94 ib_lower_bound_is_lower_bound: is_lower_bound ? a ib_lower_bound
97 record is_bounded_above (O:excedence) (a:sequence O) : Type ≝
99 ib_upper_bound_is_upper_bound: is_upper_bound ? a ib_upper_bound
102 record is_bounded (O:excedence) (a:sequence O) : Type ≝
103 { ib_bounded_below:> is_bounded_below ? a;
104 ib_bounded_above:> is_bounded_above ? a
107 record bounded_below_sequence (O:excedence) : Type ≝
108 { bbs_seq:> sequence O;
109 bbs_is_bounded_below:> is_bounded_below ? bbs_seq
112 record bounded_above_sequence (O:excedence) : Type ≝
113 { bas_seq:> sequence O;
114 bas_is_bounded_above:> is_bounded_above ? bas_seq
117 record bounded_sequence (O:excedence) : Type ≝
118 { bs_seq:> sequence O;
119 bs_is_bounded_below: is_bounded_below ? bs_seq;
120 bs_is_bounded_above: is_bounded_above ? bs_seq
123 definition bounded_below_sequence_of_bounded_sequence ≝
124 λO:excedence.λb:bounded_sequence O.
125 mk_bounded_below_sequence ? b (bs_is_bounded_below ? b).
127 coercion cic:/matita/sequence/bounded_below_sequence_of_bounded_sequence.con.
129 definition bounded_above_sequence_of_bounded_sequence ≝
130 λO:excedence.λb:bounded_sequence O.
131 mk_bounded_above_sequence ? b (bs_is_bounded_above ? b).
133 coercion cic:/matita/sequence/bounded_above_sequence_of_bounded_sequence.con.
135 definition lower_bound ≝
136 λO:excedence.λb:bounded_below_sequence O.
137 ib_lower_bound ? b (bbs_is_bounded_below ? b).
139 lemma lower_bound_is_lower_bound:
140 ∀O:excedence.∀b:bounded_below_sequence O.
141 is_lower_bound ? b (lower_bound ? b).
142 intros; unfold lower_bound; apply ib_lower_bound_is_lower_bound.
145 definition upper_bound ≝
146 λO:excedence.λb:bounded_above_sequence O.
147 ib_upper_bound ? b (bas_is_bounded_above ? b).
149 lemma upper_bound_is_upper_bound:
150 ∀O:excedence.∀b:bounded_above_sequence O.
151 is_upper_bound ? b (upper_bound ? b).
152 intros; unfold upper_bound; apply ib_upper_bound_is_upper_bound.
155 definition reverse_excedence: excedence → excedence.
156 intros (E); apply (mk_excedence E); [apply (λx,y.exc_relation E y x)]
157 cases E (T f cRf cTf); simplify;
158 [1: unfold Not; intros (x H); apply (cRf x); assumption
159 |2: intros (x y z); apply Or_symmetric; apply cTf; assumption;]
162 definition reverse_excedence: excedence → excedence.
163 intros (p); apply (mk_excedence (reverse_excedence p));
164 generalize in match (reverse_excedence p); intros (E);
165 apply mk_is_porder_relation;
166 [apply le_reflexive|apply le_transitive|apply le_antisymmetric]
169 lemma is_lower_bound_reverse_is_upper_bound:
170 ∀O:excedence.∀a:sequence O.∀l:O.
171 is_lower_bound O a l → is_upper_bound (reverse_excedence O) a l.
172 intros (O a l H); unfold; intros (n); unfold reverse_excedence;
173 unfold reverse_excedence; simplify; fold unfold le (le ? l (a n)); apply H;
176 lemma is_upper_bound_reverse_is_lower_bound:
177 ∀O:excedence.∀a:sequence O.∀l:O.
178 is_upper_bound O a l → is_lower_bound (reverse_excedence O) a l.
179 intros (O a l H); unfold; intros (n); unfold reverse_excedence;
180 unfold reverse_excedence; simplify; fold unfold le (le ? (a n) l); apply H;
183 lemma reverse_is_lower_bound_is_upper_bound:
184 ∀O:excedence.∀a:sequence O.∀l:O.
185 is_lower_bound (reverse_excedence O) a l → is_upper_bound O a l.
186 intros (O a l H); unfold; intros (n); unfold reverse_excedence in H;
187 unfold reverse_excedence in H; simplify in H; apply H;
190 lemma reverse_is_upper_bound_is_lower_bound:
191 ∀O:excedence.∀a:sequence O.∀l:O.
192 is_upper_bound (reverse_excedence O) a l → is_lower_bound O a l.
193 intros (O a l H); unfold; intros (n); unfold reverse_excedence in H;
194 unfold reverse_excedence in H; simplify in H; apply H;
197 lemma is_inf_to_reverse_is_sup:
198 ∀O:excedence.∀a:bounded_below_sequence O.∀l:O.
199 is_inf O a l → is_sup (reverse_excedence O) a l.
200 intros (O a l H); apply (mk_is_sup (reverse_excedence O));
201 [1: apply is_lower_bound_reverse_is_upper_bound; apply inf_lower_bound; assumption
202 |2: unfold reverse_excedence; simplify; unfold reverse_excedence; simplify;
203 intros (m H1); apply (inf_greatest_lower_bound ? ? ? H); apply H1;]
206 lemma is_sup_to_reverse_is_inf:
207 ∀O:excedence.∀a:bounded_above_sequence O.∀l:O.
208 is_sup O a l → is_inf (reverse_excedence O) a l.
209 intros (O a l H); apply (mk_is_inf (reverse_excedence O));
210 [1: apply is_upper_bound_reverse_is_lower_bound; apply sup_upper_bound; assumption
211 |2: unfold reverse_excedence; simplify; unfold reverse_excedence; simplify;
212 intros (m H1); apply (sup_least_upper_bound ? ? ? H); apply H1;]
215 lemma reverse_is_sup_to_is_inf:
216 ∀O:excedence.∀a:bounded_above_sequence O.∀l:O.
217 is_sup (reverse_excedence O) a l → is_inf O a l.
218 intros (O a l H); apply mk_is_inf;
219 [1: apply reverse_is_upper_bound_is_lower_bound;
220 apply (sup_upper_bound (reverse_excedence O)); assumption
221 |2: intros (v H1); apply (sup_least_upper_bound (reverse_excedence O) a l H v);
222 apply is_lower_bound_reverse_is_upper_bound; assumption;]
225 lemma reverse_is_inf_to_is_sup:
226 ∀O:excedence.∀a:bounded_above_sequence O.∀l:O.
227 is_inf (reverse_excedence O) a l → is_sup O a l.
228 intros (O a l H); apply mk_is_sup;
229 [1: apply reverse_is_lower_bound_is_upper_bound;
230 apply (inf_lower_bound (reverse_excedence O)); assumption
231 |2: intros (v H1); apply (inf_greatest_lower_bound (reverse_excedence O) a l H v);
232 apply is_upper_bound_reverse_is_lower_bound; assumption;]