]> matita.cs.unibo.it Git - helm.git/blob - matita/dama/ordered_sets2.ma
26e1cdb3f30767cf273cdce5d6b423abf70311ba
[helm.git] / matita / dama / ordered_sets2.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 set "baseuri" "cic:/matita/ordered_sets2".
16
17 include "ordered_sets.ma".
18
19 theorem le_f_inf_inf_f:
20  ∀C.∀O':dedekind_sigma_complete_ordered_set C.
21   ∀f:O'→O'. ∀H:is_order_continuous ? ? f.
22    ∀a:bounded_below_sequence ? O'.
23     let p := ? in
24      f (inf ? ? a) ≤ inf ? ? (mk_bounded_below_sequence ? ? (λi. f (a i)) p).
25  [ apply mk_is_bounded_below;
26     [2: apply ioc_is_lower_bound_f_inf;
27         assumption
28     | skip
29     ] 
30  | intros;
31    clearbody p;
32    apply (inf_greatest_lower_bound ? ? ? ? (inf_is_inf ? ? ?));
33    simplify;
34    intro;
35    letin b := (λi.match i with [ O ⇒ inf ? ? a | S _ ⇒ a n]);
36    change with (f (b O) ≤ f (b (S O)));
37    apply (ioc_is_sequentially_monotone ? ? ? H);
38    simplify;
39    clear b;
40    intro;
41    elim n1; simplify;
42     [ apply (inf_lower_bound ? ? ? ? (inf_is_inf ? ? ?));
43     | apply (or_reflexive ? O' (dscos_ordered_set ? O'))
44     ]
45  ].
46 qed.
47
48 theorem le_to_le_sup_sup:
49  ∀C.∀O':dedekind_sigma_complete_ordered_set C.
50   ∀a,b:bounded_above_sequence ? O'.
51    (∀i.a i ≤ b i) → sup ? ? a ≤ sup ? ? b.
52  intros;
53  apply (sup_least_upper_bound ? ? ? ? (sup_is_sup ? ? a));
54  unfold;
55  intro;
56  apply (or_transitive ? ? O');
57   [2: apply H
58   | skip
59   | apply (sup_upper_bound ? ? ? ? (sup_is_sup ? ? b))
60   ].
61 qed. 
62
63 interpretation "mk_bounded_sequence" 'hide_everything_but a
64 = (cic:/matita/ordered_sets/bounded_sequence.ind#xpointer(1/1/1) _ _ a _ _).
65
66 lemma reduce_bas_seq:
67  ∀C.∀O:ordered_set C.∀a:nat→O.∀p.∀i.
68   bas_seq ? ? (mk_bounded_above_sequence ? ? a p) i = a i.
69  intros;
70  reflexivity.
71 qed.
72
73 (*lemma reduce_bbs_seq:
74  ∀C.∀O:ordered_set C.∀a:nat→O.∀p.∀i.
75   bbs_seq ? ? (mk_bounded_below_sequence ? ? a p) i = a i.
76  intros;
77  reflexivity.
78 qed.*)
79
80 axiom inf_extensional:
81  ∀C.∀O:dedekind_sigma_complete_ordered_set C.
82   ∀a,b:bounded_below_sequence ? O.
83    (∀i.a i = b i) → inf ? ? a = inf ? O b.
84    
85 lemma eq_to_le: ∀C.∀O:ordered_set C.∀x,y:O.x=y → x ≤ y.
86  intros;
87  rewrite > H;
88  apply (or_reflexive ? ? O).
89 qed.
90
91 theorem fatou:
92  ∀C.∀O':dedekind_sigma_complete_ordered_set C.
93   ∀f:O'→O'. ∀H:is_order_continuous ? ? f.
94    ∀a:bounded_sequence ? O'.
95     let pb := ? in
96     let pa := ? in
97      f (liminf ? ? a) ≤ liminf ? ? (mk_bounded_sequence ? ? (λi. f (a i)) pb pa).
98  [ letin bas ≝ (bounded_above_sequence_of_bounded_sequence ? ? a);
99    apply mk_is_bounded_above;
100     [2: apply (ioc_is_upper_bound_f_sup ? ? ? H bas)
101     | skip
102     ]
103  | letin bbs ≝ (bounded_below_sequence_of_bounded_sequence ? ? a);
104    apply mk_is_bounded_below;
105     [2: apply (ioc_is_lower_bound_f_inf ? ? ? H bbs)
106     | skip
107     ] 
108  | intros;
109    rewrite > eq_f_liminf_sup_f_inf in ⊢ (? ? ? % ?);
110     [ unfold liminf;
111       apply le_to_le_sup_sup;
112       intro;
113       rewrite > reduce_bas_seq;
114       rewrite > reduce_bas_seq;
115       apply (or_transitive ? O' O');
116        [2: apply le_f_inf_inf_f;
117            assumption
118        | skip
119        | apply eq_to_le;
120          apply inf_extensional;
121          intro;
122          reflexivity
123        ]
124     | assumption
125     ]
126  ].
127 qed.