X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcontribs%2Fdama%2Fdama%2Fclassical_pointfree%2Fordered_sets2.ma;fp=matita%2Fcontribs%2Fdama%2Fdama%2Fclassical_pointfree%2Fordered_sets2.ma;h=7e74cbba2a0b038d878a49d605b269dfd4a64157;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/contribs/dama/dama/classical_pointfree/ordered_sets2.ma b/matita/contribs/dama/dama/classical_pointfree/ordered_sets2.ma
new file mode 100644
index 000000000..7e74cbba2
--- /dev/null
+++ b/matita/contribs/dama/dama/classical_pointfree/ordered_sets2.ma
@@ -0,0 +1,127 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+
+include "classical_pointfree/ordered_sets.ma".
+
+theorem le_f_inf_inf_f:
+ ∀O':dedekind_sigma_complete_ordered_set.
+  ∀f:O'→O'. ∀H:is_order_continuous ? f.
+   ∀a:bounded_below_sequence O'.
+    let p := ? in
+     f (inf ? a) ≤ inf ? (mk_bounded_below_sequence ? (λi. f (a i)) p).
+ [ apply mk_is_bounded_below;
+    [2: apply ioc_is_lower_bound_f_inf;
+        assumption
+    | skip
+    ] 
+ | intros;
+   clearbody p;
+   apply (inf_greatest_lower_bound ? ? ? (inf_is_inf ? ?));
+   simplify;
+   intro;
+   letin b := (λi.match i with [ O ⇒ inf ? a | S _ ⇒ a n]);
+   change with (f (b O) ≤ f (b (S O)));
+   apply (ioc_is_sequentially_monotone ? ? H);
+   simplify;
+   clear b;
+   intro;
+   elim n1; simplify;
+    [ apply (inf_lower_bound ? ? ? (inf_is_inf ? ?));
+    | apply (or_reflexive O' ? (dscos_ordered_set O'))
+    ]
+ ].
+qed.
+
+theorem le_to_le_sup_sup:
+ ∀O':dedekind_sigma_complete_ordered_set.
+  ∀a,b:bounded_above_sequence O'.
+   (∀i.a i ≤ b i) → sup ? a ≤ sup ? b.
+ intros;
+ apply (sup_least_upper_bound ? ? ? (sup_is_sup ? a));
+ unfold;
+ intro;
+ apply (or_transitive ? ? O');
+  [2: apply H
+  | skip
+  | apply (sup_upper_bound ? ? ? (sup_is_sup ? b))
+  ].
+qed. 
+
+interpretation "mk_bounded_sequence" 'hide_everything_but a
+= (cic:/matita/classical_pointfree/ordered_sets/bounded_sequence.ind#xpointer(1/1/1) _ _ a _ _).
+
+lemma reduce_bas_seq:
+ ∀O:ordered_set.∀a:nat→O.∀p.∀i.
+  bas_seq ? (mk_bounded_above_sequence ? a p) i = a i.
+ intros;
+ reflexivity.
+qed.
+
+(*lemma reduce_bbs_seq:
+ ∀C.∀O:ordered_set C.∀a:nat→O.∀p.∀i.
+  bbs_seq ? ? (mk_bounded_below_sequence ? ? a p) i = a i.
+ intros;
+ reflexivity.
+qed.*)
+
+axiom inf_extensional:
+ ∀O:dedekind_sigma_complete_ordered_set.
+  ∀a,b:bounded_below_sequence O.
+   (∀i.a i = b i) → inf ? a = inf O b.
+   
+lemma eq_to_le: ∀O:ordered_set.∀x,y:O.x=y → x ≤ y.
+ intros;
+ rewrite > H;
+ apply (or_reflexive ? ? O).
+qed.
+
+theorem fatou:
+ ∀O':dedekind_sigma_complete_ordered_set.
+  ∀f:O'→O'. ∀H:is_order_continuous ? f.
+   ∀a:bounded_sequence O'.
+    let pb := ? in
+    let pa := ? in
+     f (liminf ? a) ≤ liminf ? (mk_bounded_sequence ? (λi. f (a i)) pb pa).
+ [ letin bas ≝ (bounded_above_sequence_of_bounded_sequence ? a);
+   apply mk_is_bounded_above;
+    [2: apply (ioc_is_upper_bound_f_sup ? ? H bas)
+    | skip
+    ]
+ | letin bbs ≝ (bounded_below_sequence_of_bounded_sequence ? a);
+   apply mk_is_bounded_below;
+    [2: apply (ioc_is_lower_bound_f_inf ? ? H bbs)
+    | skip
+    ] 
+ | intros;
+   rewrite > eq_f_liminf_sup_f_inf in ⊢ (? ? % ?);
+    [ unfold liminf;
+      apply le_to_le_sup_sup;
+      intro;
+      rewrite > reduce_bas_seq;
+      rewrite > reduce_bas_seq;
+      apply (or_transitive ? ? O');
+       [2: apply le_f_inf_inf_f;
+           assumption
+       | skip
+       | apply eq_to_le;
+         apply inf_extensional;
+         intro;
+         reflexivity
+       ]
+    | assumption
+    ]
+ ].
+qed.