From: Enrico Tassi Date: Thu, 5 Jun 2008 15:41:15 +0000 (+0000) Subject: added order_continuity X-Git-Tag: make_still_working~5083 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=28bcf58da6b3726320b368ce4d1d8e2356b4df1b;p=helm.git 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 34b33d0ac..63f263d27 100644 --- 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 df66b8b8c..abccb351b 100644 --- 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;]]