From 7e9bcf66cf96265ea78b3de6dc95ff3c9b75f83d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 9 Jun 2008 08:24:27 +0000 Subject: [PATCH] exhaustivity, some work --- .../contribs/dama/dama/property_exhaustivity.ma | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) 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 -- 2.39.2