From c00f22f7afa508881c8d116928e1c460600ba0ac Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 10 Jun 2008 07:24:46 +0000 Subject: [PATCH] snapshot --- .../matita/contribs/dama/dama/lebesgue.ma | 17 ++++++++++++++--- .../matita/contribs/dama/dama/property_sigma.ma | 5 ++++- 2 files changed, 18 insertions(+), 4 deletions(-) diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma index 85f686da3..1b34801d2 100644 --- a/helm/software/matita/contribs/dama/dama/lebesgue.ma +++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma @@ -16,8 +16,18 @@ include "sandwich.ma". include "property_exhaustivity.ma". -le x_i e y_i stanno o no nel segmento? - +lemma foo: + ∀C:ordered_set. + ∀a:sequence C.∀l,u:C.∀H:∀i:nat.a i ∈ [l,u]. + ∀x:C.∀p:a order_converges x. + ∀j.l ≤ (match p with [ex_introT xi _ ⇒ xi] j). +intros; cases p; simplify; cases H1; clear H1; cases H2; clear H2; +cases (H3 j); cases H1; clear H3 H1; clear H4 H6; cases H5; clear H5; +cases H2; clear H2; intro; cases (H5 ? H2); +cases (H (w2+j)); apply (H8 H6); +qed. + + (* Theorem 3.10 *) theorem lebesgue: ∀C:ordered_uniform_space. @@ -34,7 +44,8 @@ theorem lebesgue: intros; cases H2 (xi H4); cases H4 (yi H5); cases H5; clear H4 H5; cases H3; cases H5; cases H4; clear H3 H4 H5 H2; split; -[2: intro h; cases (H l u (λn:nat.sig_in ?? (a n) (H1 n)) (sig_in ?? x h)); +[2: intro h; + cases (H l u (λn:nat.sig_in ?? (a n) (H1 n)) (sig_in ?? x h)); (* Theorem 3.9 *) diff --git a/helm/software/matita/contribs/dama/dama/property_sigma.ma b/helm/software/matita/contribs/dama/dama/property_sigma.ma index 691d21045..f6a315c82 100644 --- a/helm/software/matita/contribs/dama/dama/property_sigma.ma +++ b/helm/software/matita/contribs/dama/dama/property_sigma.ma @@ -112,7 +112,10 @@ lapply (H9 ?? H10) as H11; [ apply (trans_increasing ?? H4); intro; whd in H12; apply (not_le_Sn_n i); apply (transitive_le ??? H12 H5)] clear H10; intros (p q r); change with (w p 〈a (m q),a (m r)〉); -generalize in match (refl_eq nat (m p)); +generalize in match (refl_eq nat (m p)); +(* +intro E; cases p in E : (? ? ? ?); +*) generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X (w1 H15); clear X; intros (H16); simplify in H16:(? ? ? %); destruct H16; apply H15; [3: apply le_n] -- 2.39.2