snapshot

diff --git a/helm/software/matita/dama/infsup.ma b/helm/software/matita/dama/infsup.ma
index c7859577a2cd49695e83104fc21f6a7675e066b3..b3babd1b5f43f3e0b5162855ac47fd3f400b4e7f 100644 (file)
--- a/helm/software/matita/dama/infsup.ma
+++ b/helm/software/matita/dama/infsup.ma
@@ -62,6 +62,18 @@ definition bnk ≝
       [ O ⇒ (shift ?? xn k) O
       | S n1 ⇒ (shift ?? xn k) (S n1) ∨ bnk_aux n1]
     in bnk_aux.
+
+notation < "'b'\sup k" non associative with precedence 50 for
+ @{ 'bnk $x $k }.
+ 
+interpretation "bnk" 'bnk x k =
+ (cic:/matita/infsup/bnk.con _ _ x k).      
+
+notation < "('b' \sup k) \sub n" non associative with precedence 50 for
+ @{ 'bnk2 $x $k $n }.
+ 
+interpretation "bnk2" 'bnk2 x k n =
+ (cic:/matita/infsup/bnk.con _ _ x k n).      
     
 lemma ank_decreasing: 
   ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k.decreasing ? (ank ?? xn k).
@@ -81,6 +93,18 @@ simplify; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
 apply meet_comm;
 qed.    
 
+lemma bnkS:
+  ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n:nat.
+   ((bnk ?? xn k) (S n)) ≈ (xn k ∨ bnk ?? xn (S k) n).
+intros (R ml xn k n); elim n; simplify; [apply join_comm]  
+simplify in H; apply (Eq≈ ? (feq_jl ???? (H))); clear H;
+apply (Eq≈ ? (join_assoc ????));    
+apply (Eq≈ ?? (eq_sym ??? (join_assoc ????)));
+apply feq_jr; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
+simplify; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
+apply join_comm;
+qed.    
+
 lemma le_asnk_ansk:
   ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n.
    (ank ?? xn k (S n)) ≤ (ank ?? xn (S k) n).
@@ -88,8 +112,18 @@ intros (R ml xn k n);
 apply (Le≪ (xn k ∧ ank ?? xn (S k) n) (ankS ?????)); apply lem;
 qed.   
 
+lemma le_bnsk_bsnk:
+  ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n.
+   (bnk ?? xn (S k) n) ≤ (bnk ?? xn k (S n)).
+intros (R ml xn k n);
+apply (Le≫ (xn k ∨ bnk ?? xn (S k) n) (bnkS ?????)); 
+apply (Le≫ ? (join_comm ???));
+apply lej;
+qed.   
+
+
 (* 3.27 *)
-lemma sup_increasing:
+lemma inf_increasing:
   ∀R.∀ml:mlattice R.∀xn:sequence ml.
    ∀alpha:sequence ml. (∀k.strong_inf ml (ank ?? xn k) (alpha k)) → 
      increasing ml alpha.
@@ -103,4 +137,65 @@ lapply (le_transitive ???? Hsw (le_asnk_ansk ?????)) as H;
 cases (H Hw);
 qed.
 
-   
\ No newline at end of file
+lemma sup_decreasing:
+  ∀R.∀ml:mlattice R.∀xn:sequence ml.
+   ∀alpha:sequence ml. (∀k.strong_sup ml (bnk ?? xn k) (alpha k)) → 
+     decreasing ml alpha.
+intros (R ml xn alpha H); unfold strong_sup in H; unfold upper_bound in H; unfold; 
+intro r; 
+elim (H r) (H1r H2r);
+elim (H (S r)) (H1sr H2sr); clear H H2r H1sr;
+intro e; cases (H2sr ? e) (w Hw); clear e H2sr;
+lapply (H1r (S w)) as Hsw; clear H1r;
+lapply (le_transitive ???? (le_bnsk_bsnk ?????) Hsw) as H;
+cases (H Hw);
+qed.
+
+(* 3.28 *)
+definition liminf ≝
+  λR.λml:mlattice R.λxn:sequence ml.λx:ml.   
+    ∃alpha:sequence ml. 
+      (∀k.strong_inf ml (ank ?? xn k) (alpha k)) ∧ strong_sup ml alpha x.
+  
+definition limsup ≝
+  λR.λml:mlattice R.λxn:sequence ml.λx:ml.   
+    ∃alpha:sequence ml. 
+      (∀k.strong_sup ml (bnk ?? xn k) (alpha k)) ∧ strong_inf ml alpha x.
+  
+(* 3.29 *)  
+alias symbol "and" = "constructive and".
+definition lim ≝
+  λR.λml:mlattice R.λxn:sequence ml.λx:ml.   
+   (*∃y,z.*)limsup ?? xn x ∧ liminf ?? xn x(* ∧ y ≈ x ∧ z ≈ x*).
+  
+(* 3.30 *)   
+lemma lim_uniq: ∀R.∀ml:mlattice R.∀xn:sequence ml.∀x:ml.
+   lim ?? xn x → xn ⇝ x.
+intros (R ml xn x Hl); 
+unfold in Hl; unfold limsup in Hl; unfold liminf in Hl; 
+(* decompose; *)
+elim Hl (low Hl_); clear Hl;   
+elim Hl_ (up Hl); clear Hl_;  
+elim Hl (Hl_ E1); clear Hl;   
+elim Hl_ (Hl E2); clear Hl_;  
+elim Hl (H1 H2); clear Hl;   
+elim H1 (alpha Halpha); clear H1;   
+elim H2 (beta Hbeta); clear H2;
+apply (sandwich ?? alpha beta); 
+[1: intro m; elim Halpha (Ha5 Ha6); clear Halpha;
+    lapply (sup_increasing ????? Ha6) as Ha7;
+
+    unfold strong_sup in Halpha Hbeta;
+    unfold strong_inf in Halpha Hbeta;
+    unfold lower_bound in Halpha Hbeta;
+    unfold upper_bound in Halpha Hbeta; 
+    elim (Halpha m) (Ha5 Ha6); clear Halpha;
+    elim Ha5 (Ha1 Ha2); clear Ha5;
+    elim Ha6 (Ha3 Ha4); clear Ha6;
+    split; 
+    [1: intro H; elim (Ha2 ? H) (w H1);
+        elim (Ha4 ? H1);
+    
+    
+    
+  
\ No newline at end of file

diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index 9b163378e80e8f6092a33f076123b413b5edadfd..fcad3fdc54dc227e4ea3cbd9c3ac7665db07b831 100644 (file)
--- a/helm/software/matita/dama/lattice.ma
+++ b/helm/software/matita/dama/lattice.ma
@@ -133,6 +133,11 @@ intros (l a b c H); unfold eq in H ⊢ %; unfold Not in H ⊢ %;
 intro H1; apply H; clear H; apply (strong_extj ???? H1);
 qed.
 
+lemma feq_jr: ∀ml:lattice.∀a,b,c:ml. a ≈ b → (a ∨ c) ≈ (b ∨ c).
+intros (l a b c H); apply (Eq≈ ? (join_comm ???)); apply (Eq≈ ?? (join_comm ???));
+apply (feq_jl ???? H);
+qed.
+
 lemma le_to_eqj: ∀ml:lattice.∀a,b:ml. a ≤ b → b ≈ (a ∨ b).
 intros (l a b H); lapply (le_to_eqm ??? H) as H1;
 lapply (feq_jl ??? b H1) as H2;
@@ -141,3 +146,8 @@ apply (Eq≈ (b∨a∧b) ? H2); clear H1 H2 H;
 apply (Eq≈ (b∨(b∧a)) ? (feq_jl ???? (meet_comm ???)));
 apply eq_sym; apply absorbjm;
 qed.
+
+lemma lej: ∀l:lattice.∀x,y:l.x ≤ (x ∨ y).
+intros (l x y); 
+apply (Le≪ ? (absorbmj ? x y)); apply lem;
+qed.
\ No newline at end of file