snapshot

[helm.git] / helm / software / matita / contribs / dama / dama / lebesgue.ma

diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma
index 85f686da3ebed0968b3e7970ee599d3fb552b9a5..1b34801d2949e2516096675c462066eeed18d7d1 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/lebesgue.ma
+++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma
@@ -16,8 +16,18 @@
 include "sandwich.ma".
 include "property_exhaustivity.ma".
 
-le x_i e y_i stanno o no nel segmento?
-
+lemma foo:
+  ∀C:ordered_set.
+   ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. 
+     ∀x:C.∀p:a order_converges x. 
+       ∀j.l ≤ (match p with [ex_introT xi _ ⇒ xi] j).
+intros; cases p; simplify; cases H1; clear H1; cases H2; clear H2;
+cases (H3 j); cases H1; clear H3 H1; clear H4 H6; cases H5; clear H5;
+cases H2; clear H2;  intro; cases (H5 ? H2);
+cases (H (w2+j)); apply (H8 H6);
+qed.   
+     
+     
 (* Theorem 3.10 *)
 theorem lebesgue:
   ∀C:ordered_uniform_space.
@@ -34,7 +44,8 @@ theorem lebesgue:
 intros; cases H2 (xi H4); cases H4 (yi H5); cases H5; clear H4 H5; 
 cases H3; cases H5; cases H4; clear H3 H4 H5 H2;
 split;
-[2: intro h; cases (H l u (λn:nat.sig_in ?? (a n) (H1 n)) (sig_in ?? x h)); 
+[2: intro h;
+  cases (H l u (λn:nat.sig_in ?? (a n) (H1 n)) (sig_in ?? x h)); 
 
 
 (* Theorem 3.9 *)