added order_continuity

diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
index 34b33d0ace284b94e03c83831ad02dde757522d4..63f263d274296119010fd9aee822fce2fab8fce9 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
@@ -139,7 +139,7 @@ interpretation "Ordered uniform space segment" 'segment_set 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 +150,7 @@ 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).
+

diff --git a/helm/software/matita/contribs/dama/dama/sandwich.ma b/helm/software/matita/contribs/dama/dama/sandwich.ma
index df66b8b8cb15e787d5cd814aa238fed0170e37c0..abccb351b14736ae1a0d7d276a228eb57937caf4 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/sandwich.ma
+++ b/helm/software/matita/contribs/dama/dama/sandwich.ma
@@ -41,7 +41,7 @@ unfold; simplify; exists [apply (a i)] split;
     |2: simplify; apply (le_transitive ???? Lax Lxb);
     |3: simplify; repeat split; try assumption; 
         [1: apply (le_transitive ???? Lax Lxb);
-        |2: (* prove le_reflexive *) intro X; cases (os_coreflexive ?? X)]]
+        |2: intro X; cases (os_coreflexive ?? X)]]
 |1: apply HW; exists[apply l] simplify; split;
     [1: apply (us_phi1 ?? Gw); unfold; apply eq_reflexive;
     |2: apply Hma;  rewrite > sym_plus in H1; apply (le_w_plus mb); assumption;]]