....

diff --git a/helm/software/matita/contribs/dama/dama/property_sigma.ma b/helm/software/matita/contribs/dama/dama/property_sigma.ma
new file mode 100644 (file)
index 0000000..7d35e08
--- /dev/null
+++ b/helm/software/matita/contribs/dama/dama/property_sigma.ma
@@ -0,0 +1,60 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "ordered_uniform.ma".
+
+
+(* Definition 3.5 *)
+alias num (instance 0) = "natural number".
+definition property_sigma ≝
+  λC:ordered_uniform_space.
+   ∀U.us_unifbase ? U → 
+     ∃V:sequence (C square → Prop).
+       (∀i.us_unifbase ? (V i)) ∧ 
+       ∀a:sequence C.∀x:C.a ↑ x → 
+         (∀n.∀i,j.n ≤ i → n ≤ j → V n 〈a i,a j〉) → U 〈a 0,x〉.
+      
+definition max ≝
+  λm,n.match leb n m with [true ⇒ m | false ⇒ n].
+  
+lemma le_max: ∀n,m.m ≤ max n m.
+intros; unfold max; apply leb_elim; simplify; intros; [assumption] apply le_n;
+qed.   
+
+definition hide ≝ λT:Type.λx:T.x.
+
+notation < "\blacksquare" non associative with precedence 50 for @{'hide}.
+interpretation "hide" 'hide =
+ (cic:/matita/dama/property_sigma/hide.con _ _).
+      
+(* Lemma 3.6 *)   
+lemma sigma_cauchy:
+  ∀O:ordered_uniform_space.property_sigma O →
+    ∀a:sequence O.∀l:O.a ↑ l → a is_cauchy → a uniform_converges l.
+intros 8; cases H1; cases H5; clear H5;
+cases (H ? H3); cases H5; clear H5;
+letin m ≝ (? : sequence nat_ordered_set); [
+  apply (hide (nat→nat)); intro i; elim i (i' Rec);
+    [1: apply (hide nat);cases (H2 ? (H8 0)) (k _); apply k;
+    |2: apply (max (hide nat ?) (S Rec)); cases (H2 ? (H8 (S i'))) (k Hk);apply k]]
+cut (m is_strictly_increasing) as Hm; [2:
+  intro n; change with (S (m n) ≤ m (S n)); unfold m; whd in ⊢ (? ? %); apply (le_max ? (S (m n)));]    
+lapply (selection ?? Hm a l H1) as H10;
+lapply (H9 ?? H10) as H11;
+[1: exists [apply (m 0)] intros;
+    apply (ous_convex ?? H3 ? H11 (H6 (m 0)));
+    simplify; repeat split;
+        
+  
+  
\ No newline at end of file