3.27 ok

diff --git a/helm/software/matita/dama/infsup.ma b/helm/software/matita/dama/infsup.ma
index 7ba29dd1bab9162554a44bad8758326b6b694a57..c7859577a2cd49695e83104fc21f6a7675e066b3 100644 (file)
--- a/helm/software/matita/dama/infsup.ma
+++ b/helm/software/matita/dama/infsup.ma
@@ -81,36 +81,26 @@ 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 foo:
+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 n;
-letin H2 ≝ (λk.ankS ?? xn k n); clearbody H2;
-cut (∀k.((xn k) ∧ (ank ?? xn (S k) n)) ≤ (ank ?? xn (S k) n)) as H3; [2:intro k; apply lem;]
-cut (∀k.(ank ?? xn k (S n)) ≤ (ank ?? xn (S k) n)) as H4; [2:
-  intro k; apply (le_transitive ml ???? (H3 ?));
-  apply (Le≪ ? (H2 k));
-
-elim (H (S n)) (H4 H5); intro H6; elim (H5 ? H6) (m Hm);
-lapply (H4 m) as H7;
-
- clear H5 H6;
-
-
-
-lapply (H n) as H1; clear H; elim H1 (LB H); clear H1;
-lapply (LB (S n)) as H1; clear LB;
-lapply (ankS ?? xn n n) as H2;
-
-lapply (Le≪ (xn n∧ank R ml xn (S n) n) H2);
-
-cases H (LB H1); clear H; 
+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

diff --git a/helm/software/matita/dama/metric_space.ma b/helm/software/matita/dama/metric_space.ma
index bd16b2bd60217b33208159b97e188c99c2b06ee3..2ea43c03ae11017df5c262218a41b570ff11c15a 100644 (file)
--- a/helm/software/matita/dama/metric_space.ma
+++ b/helm/software/matita/dama/metric_space.ma
@@ -49,5 +49,5 @@ qed.
     
 (* coercion cic:/matita/metric_space/apart_of_metric_space.con. *)
 
-lemma ap2delta: ∀R.∀m:metric_space R.∀x,y:m.x#y → 0 < δ x y.
+lemma ap2delta: ∀R.∀m:metric_space R.∀x,y:m.ap_apart (apart_of_metric_space ? m) x y → 0 < δ x y.
 intros 2 (R m); cases m 0; simplify; intros; assumption; qed.