exhaustivity, some work

diff --git a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
index 00f8cb25917339cc960f25c510f5b5a4a00b31c8..173739f27853b69db8dcbe8dd89fa5e5b9b48346 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
+++ b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
@@ -13,12 +13,22 @@
 (**************************************************************************)
 
 include "ordered_uniform.ma".
+include "property_sigma.ma".
 
 (* Definition 3.7 *)
-definition exhaustivity ≝
+definition exhaustive ≝
   λC:ordered_uniform_space.
    ∀a,b:sequence C.
      (a is_increasing → a is_upper_located → a is_cauchy) ∧
      (b is_decreasing → b is_lower_located → b is_cauchy).
      
 (* Lemma 3.8 *)
+lemma xxx:
+  ∀C:ordered_uniform_space.property_sigma C →
+    ∀l,u:C.exhaustive {[l,u]} →
+     ∀a:sequence {[l,u]}.∀x:C. (λn.fst (a n)) ↑ x → 
+      x∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges (sig_in ?? x h).
+intros; split;
+[1: (* manca fact 2.5 *)
+      
+       
\ No newline at end of file