X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Finfsup.ma;h=cc3292fd0b5178775d5199ba3bc5d850570a6e38;hb=2b422d5f721aacb242951118188f376bf1dc7ce2;hp=c7859577a2cd49695e83104fc21f6a7675e066b3;hpb=083ff2fab06a904ec21f610311134b8b3ee32c67;p=helm.git

diff --git a/helm/software/matita/dama/infsup.ma b/helm/software/matita/dama/infsup.ma
index c7859577a..cc3292fd0 100644
--- a/helm/software/matita/dama/infsup.ma
+++ b/helm/software/matita/dama/infsup.ma
@@ -12,95 +12,42 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "sandwich_corollary.ma".
-
-(* 3.19 *)
-definition supremum ≝ 
-  λR.λml:mlattice R.λxn:sequence ml.λx:ml.
-    increasing ? xn → upper_bound ? xn x ∧ xn ⇝ x.
-
-definition infimum ≝ 
-  λR.λml:mlattice R.λxn:sequence ml.λx:ml.
-    decreasing ? xn → lower_bound ? xn x ∧ xn ⇝ x.
-    
-(* 3.20 *)
-lemma supremum_uniq:
-  ∀R.∀ml:mlattice R.∀xn:sequence ml.increasing ? xn → 
-   ∀x,y:ml.supremum ?? xn x → supremum ?? xn y → δ x y ≈ 0.
-intros (R ml xn Hxn x y Sx Sy);
-elim (Sx Hxn) (_ Hx); elim (Sy Hxn) (_ Hy);
-apply (tends_uniq ?? xn ?? Hx Hy);
-qed.
-
-definition shift : ∀R.∀ml:mlattice R.∀xn:sequence ml.nat → sequence ml ≝
- λR.λml:mlattice R.λxn:sequence ml.λm:nat.λn.xn (n+m).
- 
-definition ank ≝
-  λR.λml:mlattice R.λxn:sequence ml.λk:nat.
-    let rec ank_aux (i : nat) ≝
-      match i with 
-      [ O ⇒ (shift ?? xn k) O
-      | S n1 ⇒ (shift ?? xn k) (S n1) ∧ ank_aux n1]
-    in ank_aux.
-     
-notation < "'a'\sup k" non associative with precedence 50 for
- @{ 'ank $x $k }.
- 
-interpretation "ank" 'ank x k =
- (cic:/matita/infsup/ank.con _ _ x k).      
-
-notation < "'a'(k \atop n)" non associative with precedence 50 for
- @{ 'ank2 $x $k $n }.
- 
-interpretation "ank2" 'ank2 x k n =
- (cic:/matita/infsup/ank.con _ _ x k n).      
-    
-definition bnk ≝
-  λR.λml:mlattice R.λxn:sequence ml.λk:nat.
-    let rec bnk_aux (i : nat) ≝
-      match i with 
-      [ O ⇒ (shift ?? xn k) O
-      | S n1 ⇒ (shift ?? xn k) (S n1) ∨ bnk_aux n1]
-    in bnk_aux.
-    
-lemma ank_decreasing: 
-  ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k.decreasing ? (ank ?? xn k).
-intros (R ml xn k); unfold; intro n; simplify; apply lem;
+include "sequence.ma".
+
+definition upper_bound ≝ λO:excess.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
+
+definition weak_sup ≝
+  λO:excess.λs:sequence O.λx.
+    upper_bound ? s x ∧ (∀y:O.upper_bound ? s y → x ≤ y).
+
+definition strong_sup ≝
+  λO:excess.λs:sequence O.λx.upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y).
+
+definition increasing ≝ λO:excess.λa:sequence O.∀n:nat.a n ≤ a (S n).
+
+notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 50 for @{'upper_bound $_ $s $x}.
+notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 50 for @{'lower_bound $_ $s $x}.
+notation < "s \nbsp 'is_increasing'"          non associative with precedence 50 for @{'increasing $_ $s}.
+notation < "s \nbsp 'is_decreasing'"          non associative with precedence 50 for @{'decreasing $_ $s}.
+notation < "x \nbsp 'is_strong_sup' \nbsp s"  non associative with precedence 50 for @{'strong_sup $_ $s $x}.
+notation < "x \nbsp 'is_strong_inf' \nbsp s"  non associative with precedence 50 for @{'strong_inf $_ $s $x}.
+
+notation > "x 'is_upper_bound' s 'in' e" non associative with precedence 50 for @{'upper_bound $e $s $x}.
+notation > "x 'is_lower_bound' s 'in' e" non associative with precedence 50 for @{'lower_bound $e $s $x}.
+notation > "s 'is_increasing' 'in' e"    non associative with precedence 50 for @{'increasing $e $s}.
+notation > "s 'is_decreasing' 'in' e"    non associative with precedence 50 for @{'decreasing $e $s}.
+notation > "x 'is_strong_sup' s 'in' e"  non associative with precedence 50 for @{'strong_sup $e $s $x}.
+notation > "x 'is_strong_inf' s 'in' e"  non associative with precedence 50 for @{'strong_inf $e $s $x}.
+
+interpretation "Excess upper bound" 'upper_bound e s x = (cic:/matita/infsup/upper_bound.con e s x).
+interpretation "Excess lower bound" 'lower_bound e s x = (cic:/matita/infsup/upper_bound.con (cic:/matita/excess/dual_exc.con e) s x).
+interpretation "Excess increasing"  'increasing e s    = (cic:/matita/infsup/increasing.con e s).
+interpretation "Excess decreasing"  'decreasing e s    = (cic:/matita/infsup/increasing.con (cic:/matita/excess/dual_exc.con e) s).
+interpretation "Excess strong sup"  'strong_sup e s x  = (cic:/matita/infsup/strong_sup.con e s x).
+interpretation "Excess strong inf"  'strong_inf e s x  = (cic:/matita/infsup/strong_sup.con (cic:/matita/excess/dual_exc.con e) s x).
+
+lemma strong_sup_is_weak: 
+  ∀O:excess.∀s:sequence O.∀x:O.strong_sup ? s x → weak_sup ? s x.
+intros (O s x Ssup); elim Ssup (Ubx M); clear Ssup; split; [assumption]
+intros 3 (y Uby E); cases (M ? E) (n En); unfold in Uby; cases (Uby ? En);
 qed.
-
-(* 3.26 *)
-lemma ankS:
-  ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n:nat.
-   ((ank ?? xn k) (S n)) ≈ (xn k ∧ ank ?? xn (S k) n).
-intros (R ml xn k n); elim n; simplify; [apply meet_comm]  
-simplify in H; apply (Eq≈ ? (feq_ml ???? (H))); clear H;
-apply (Eq≈ ? (meet_assoc ????));    
-apply (Eq≈ ?? (eq_sym ??? (meet_assoc ????)));
-apply feq_mr; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
-simplify; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
-apply meet_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).
-intros (R ml xn k n);
-apply (Le≪ (xn k ∧ ank ?? xn (S k) n) (ankS ?????)); apply lem;
-qed.   
-
-(* 3.27 *)
-lemma sup_increasing:
-  ∀R.∀ml:mlattice R.∀xn:sequence ml.
-   ∀alpha:sequence ml. (∀k.strong_inf ml (ank ?? xn k) (alpha k)) → 
-     increasing ml alpha.
-intros (R ml xn alpha H); unfold strong_inf in H; unfold lower_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 ???? Hsw (le_asnk_ansk ?????)) as H;
-cases (H Hw);
-qed.
-
-   
\ No newline at end of file