LambdaDelta-1 regenerated as a subdevel ov LAMBDA-TYPES

[helm.git] / helm / software / matita / dama / limit.ma

diff --git a/helm/software/matita/dama/limit.ma b/helm/software/matita/dama/limit.ma
index 14a0637b35c4e5d58ee1edc5fd1ad3d87b4bcee8..1250511e83ddda1573c8df1feca7b1d58878f74e 100644 (file)
--- a/helm/software/matita/dama/limit.ma
+++ b/helm/software/matita/dama/limit.ma
@@ -14,30 +14,34 @@
 
 include "infsup.ma".
 
+definition shift ≝ λT:Type.λs:sequence T.λk:nat.λn.s (n+k).
+
 (* 3.28 *)
 definition limsup ≝
   λE:excess.λxn:sequence E.λx:E.∃alpha:sequence E. 
-    (∀k.(alpha k) is_strong_sup xn) ∧ x is_strong_inf alpha.
+    (∀k.(alpha k) is_strong_sup (shift ? xn k) in E) ∧ 
+     x is_strong_inf alpha in E.     
 
-notation < "x \nbsp 'is_limsup' \nbsp s" non associative with precedence 50 for @{'limsup $s $x}.
-notation < "x \nbsp 'is_liminf' \nbsp s" non associative with precedence 50 for @{'liminf $s $x}.
-notation > "x 'is_limsup' s" non associative with precedence 50 for @{'limsup $s $x}.
-notation > "x 'is_liminf' s" non associative with precedence 50 for @{'liminf $s $x}.
+notation < "x \nbsp 'is_limsup' \nbsp s" non associative with precedence 50 for @{'limsup $_ $s $x}.
+notation < "x \nbsp 'is_liminf' \nbsp s" non associative with precedence 50 for @{'liminf $_ $s $x}.
+notation > "x 'is_limsup' s 'in' e" non associative with precedence 50 for @{'limsup $e $s $x}.
+notation > "x 'is_liminf' s 'in' e" non associative with precedence 50 for @{'liminf $e $s $x}.
 
-interpretation "Excess limsup" 'limsup s x = (cic:/matita/limit/limsup.con _ s x).
-interpretation "Excess liminf" 'liminf s x = (cic:/matita/limit/limsup.con (cic:/matita/excess/dual_exc.con _) s x).
+interpretation "Excess limsup" 'limsup e s x = (cic:/matita/limit/limsup.con e s x).
+interpretation "Excess liminf" 'liminf e s x = (cic:/matita/limit/limsup.con (cic:/matita/excess/dual_exc.con e) s x).
 
 (* 3.29 *)  
-definition lim ≝ λE:excess.λxn:sequence E.λx:E. x is_limsup xn ∧ x is_liminf xn.
+definition lim ≝ 
+  λE:excess.λxn:sequence E.λx:E. x is_limsup xn in E ∧ x is_liminf xn in E.
 
-notation < "x \nbsp 'is_lim' \nbsp s" non associative with precedence 50 for @{'lim $s $x}.
-notation > "x 'is_lim' s" non associative with precedence 50 for @{'lim $s $x}.
-interpretation "Excess lim" 'lim s x = (cic:/matita/limit/lim.con _ s x).
+notation < "x \nbsp 'is_lim' \nbsp s" non associative with precedence 50 for @{'lim $_ $s $x}.
+notation > "x 'is_lim' s 'in' e" non associative with precedence 50 for @{'lim $e $s $x}.
+interpretation "Excess lim" 'lim e s x = (cic:/matita/limit/lim.con e s x).
 
 lemma sup_decreasing:
   ∀E:excess.∀xn:sequence E.
-   ∀alpha:sequence E. (∀k.(alpha k) is_strong_sup xn) → 
-     alpha is_decreasing.
+   ∀alpha:sequence E. (∀k.(alpha k) is_strong_sup xn in E) → 
+     alpha is_decreasing in E.
 intros (E xn alpha H); unfold strong_sup in H; unfold upper_bound in H; unfold;
 intro r; 
 elim (H r) (H1r H2r);
@@ -47,10 +51,17 @@ cases (H1r w Hw);
 qed.
 
 include "tend.ma".
+include "metric_lattice.ma".
   
 (* 3.30 *)   
 lemma lim_tends: 
   ∀R.∀ml:mlattice R.∀xn:sequence ml.∀x:ml.
-    x is_lim xn → xn ⇝ x.
+    x is_lim xn in ml → xn ⇝ x.
 intros (R ml xn x Hl); unfold lim in Hl; unfold limsup in Hl;
-
+cases Hl (e1 e2); cases e1 (an Han); cases e2 (bn Hbn); clear Hl e1 e2;
+cases Han (SSan SIxan); cases Hbn (SSbn SIxbn); clear Han Hbn;
+cases SIxan (LBxan Hxg); cases SIxbn (UPxbn Hxl); clear SIxbn SIxan;
+change in UPxbn:(%) with (x is_lower_bound bn in ml);
+unfold upper_bound in UPxbn LBxan; change  
+intros (e He);  
+(* 2.6 OC *)