From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 9 Jun 2008 08:24:27 +0000 (+0000)
Subject: exhaustivity, some work
X-Git-Tag: make_still_working~5053
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7e9bcf66cf96265ea78b3de6dc95ff3c9b75f83d;p=helm.git

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 00f8cb259..173739f27 100644
--- 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