X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fordered_uniform.ma;h=1ca01611f66dd3b29e81269efc39ce640c2841e5;hb=9eabe046c1182960de8cfdba96c5414224e3a61e;hp=34b33d0ace284b94e03c83831ad02dde757522d4;hpb=cb4d4678ada706caaf8c54f2d6780c228645f911;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
index 34b33d0ac..1ca01611f 100644
--- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
@@ -86,8 +86,7 @@ lemma bs_of_ss:
  λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉.
 
 notation < "x \sub \neq" non associative with precedence 91 for @{'bsss $x}.
-interpretation "bs_of_ss" 'bsss x = 
-  (cic:/matita/dama/ordered_uniform/bs_of_ss.con _ _ _ x).
+interpretation "bs_of_ss" 'bsss x = (bs_of_ss _ _ _ x).
 
 lemma segment_ordered_uniform_space: 
   ∀O:ordered_uniform_space.∀u,v:O.ordered_uniform_space.
@@ -135,11 +134,11 @@ intros (O l r); apply mk_ordered_uniform_space;
 qed.
 
 interpretation "Ordered uniform space segment" 'segment_set a b = 
- (cic:/matita/dama/ordered_uniform/segment_ordered_uniform_space.con _ a b).
+ (segment_ordered_uniform_space _ a b).
 
 (* Lemma 3.2 *)
 alias symbol "pi1" = "sigma pi1".
-lemma foo:
+lemma restric_uniform_convergence:
  ∀O:ordered_uniform_space.∀l,u:O.
   ∀x:{[l,u]}.
    ∀a:sequence {[l,u]}.
@@ -150,3 +149,6 @@ cases (H ? H3) (m Hm); exists [apply m]; intros;
 apply (restrict ? l u ??? H4); apply (Hm ? H1);
 qed.
 
+definition order_continuity ≝
+  λC:ordered_uniform_space.∀a:sequence C.∀x:C.
+    (a ↑ x → a uniform_converges x) ∧ (a ↓ x → a uniform_converges x).