From: Enrico Zoli <??>
Date: Fri, 15 Dec 2006 16:11:56 +0000 (+0000)
Subject: Fatou lemma achieved (up to a few more axioms here and there...)
X-Git-Tag: 0.4.95@7852~727
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e04738d23c02ea5d6b8a66372e6d62b73f52e2db;p=helm.git

Fatou lemma achieved (up to a few more axioms here and there...)
---

diff --git a/matita/dama/ordered_sets2.ma b/matita/dama/ordered_sets2.ma
index b597d372c..26e1cdb3f 100644
--- a/matita/dama/ordered_sets2.ma
+++ b/matita/dama/ordered_sets2.ma
@@ -63,6 +63,31 @@ qed.
 interpretation "mk_bounded_sequence" 'hide_everything_but a
 = (cic:/matita/ordered_sets/bounded_sequence.ind#xpointer(1/1/1) _ _ a _ _).
 
+lemma reduce_bas_seq:
+ ∀C.∀O:ordered_set C.∀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:
+ ∀C.∀O:dedekind_sigma_complete_ordered_set C.
+  ∀a,b:bounded_below_sequence ? O.
+   (∀i.a i = b i) → inf ? ? a = inf ? O b.
+   
+lemma eq_to_le: ∀C.∀O:ordered_set C.∀x,y:O.x=y → x ≤ y.
+ intros;
+ rewrite > H;
+ apply (or_reflexive ? ? O).
+qed.
+
 theorem fatou:
  ∀C.∀O':dedekind_sigma_complete_ordered_set C.
   ∀f:O'→O'. ∀H:is_order_continuous ? ? f.
@@ -81,11 +106,21 @@ theorem fatou:
     | skip
     ] 
  | intros;
-   rewrite > eq_f_liminf_sup_f_inf;
+   rewrite > eq_f_liminf_sup_f_inf in ⊢ (? ? ? % ?);
     [ unfold liminf;
       apply le_to_le_sup_sup;
-      elim daemon (*(* f inf < inf f *)
-      apply le_f_inf_inf_f*)
+      intro;
+      rewrite > reduce_bas_seq;
+      rewrite > reduce_bas_seq;
+      apply (or_transitive ? O' O');
+       [2: apply le_f_inf_inf_f;
+           assumption
+       | skip
+       | apply eq_to_le;
+         apply inf_extensional;
+         intro;
+         reflexivity
+       ]
     | assumption
     ]
  ].