From: Enrico Tassi Date: Thu, 23 Oct 2008 09:13:44 +0000 (+0000) Subject: lebesgue completely dualized X-Git-Tag: make_still_working~4643 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=82d281529c1a9450ac213a058e7f8c0e228026fa;p=helm.git lebesgue completely dualized --- diff --git a/helm/software/matita/contribs/dama/dama/ordered_set.ma b/helm/software/matita/contribs/dama/dama/ordered_set.ma index 7008b632b..233df16f6 100644 --- a/helm/software/matita/contribs/dama/dama/ordered_set.ma +++ b/helm/software/matita/contribs/dama/dama/ordered_set.ma @@ -42,13 +42,29 @@ intro; constructor 1; qed. record ordered_set : Type ≝ { - os_l : half_ordered_set; + os_l_ : half_ordered_set; os_r_ : half_ordered_set; - os_with : os_r_ = dual_hos os_l + os_with : os_r_ = dual_hos os_l_ }. +definition os_l : ordered_set → half_ordered_set. +intro h; constructor 1; +[ apply (hos_carr (os_l_ h)); +| apply (λx,y.hos_excess (os_l_ h) x y); +| apply (hos_coreflexive (os_l_ h)); +| apply (hos_cotransitive (os_l_ h)); +] +qed. + definition os_r : ordered_set → half_ordered_set. -intro o; apply (dual_hos (os_l o)); qed. +intro o; apply (dual_hos (os_l_ o)); qed. + +lemma half2full : half_ordered_set → ordered_set. +intro hos; +constructor 1; [apply hos; | apply (dual_hos hos); | reflexivity] +qed. + +(* coercion half2full. *) definition Type_of_ordered_set : ordered_set → Type. intro o; apply (hos_carr (os_l o)); qed. diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma index 8cca24c90..701651cb1 100644 --- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma +++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma @@ -163,35 +163,6 @@ cases (H ? H3) (m Hm); exists [apply m]; intros; apply (restrict ? l u ??? H4); apply (Hm ? H1); qed. -definition hint_sequence: - ∀C:ordered_set. - sequence (hos_carr (os_l C)) → sequence (Type_of_ordered_set C). -intros;assumption; -qed. - -definition hint_sequence1: - ∀C:ordered_set. - sequence (hos_carr (os_r C)) → sequence (Type_of_ordered_set_dual C). -intros;assumption; -qed. - -definition hint_sequence2: - ∀C:ordered_set. - sequence (Type_of_ordered_set C) → sequence (hos_carr (os_l C)). -intros;assumption; -qed. - -definition hint_sequence3: - ∀C:ordered_set. - sequence (Type_of_ordered_set_dual C) → sequence (hos_carr (os_r C)). -intros;assumption; -qed. - -coercion hint_sequence nocomposites. -coercion hint_sequence1 nocomposites. -coercion hint_sequence2 nocomposites. -coercion hint_sequence3 nocomposites. - 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/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma index 96170fa26..41674ec00 100644 --- a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma +++ b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma @@ -76,7 +76,7 @@ intros; cases H2 (Ha Hx); clear H2; cases Hx; split; |2: intros; lapply (uparrow_upperlocated a ≪x,h≫) as Ha1; [2: apply (segment_preserves_uparrow C l u);split; assumption;] - lapply (segment_preserves_supremum l u a ≪?,h≫) as Ha2; + lapply (segment_preserves_supremum C l u a ≪?,h≫) as Ha2; [2:split; assumption]; cases Ha2; clear Ha2; cases (H1 a a); lapply (H6 H4 Ha1) as HaC; lapply (segment_cauchy ? l u ? HaC) as Ha; @@ -108,12 +108,11 @@ lemma hint_mah4: coercion hint_mah4 nocomposites. -axiom restrict_uniform_convergence_downarrow: +lemma restrict_uniform_convergence_downarrow: ∀C:ordered_uniform_space.property_sigma C → ∀l,u:C.exhaustive {[l,u]} → ∀a:sequence {[l,u]}.∀x: C. ⌊n,\fst (a n)⌋ ↓ x → x∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges ≪x,h≫. - (* intros; cases H2 (Ha Hx); clear H2; cases Hx; split; [1: split; [2: apply (infimum_is_lower_bound ? x Hx l); @@ -122,13 +121,11 @@ intros; cases H2 (Ha Hx); clear H2; cases Hx; split; apply (segment_upperbound ? l u a 0);] |2: intros; lapply (downarrow_lowerlocated a ≪x,h≫) as Ha1; - [2: apply (segment_preserves_downarrow ? l u);split; assumption;] - lapply (segment_preserves_infimum l u); - [2: apply a; ≪?,h≫) as Ha2; + [2: apply (segment_preserves_downarrow ? l u);split; assumption;] + lapply (segment_preserves_infimum C l u a ≪x,h≫) as Ha2; [2:split; assumption]; cases Ha2; clear Ha2; cases (H1 a a); lapply (H7 H4 Ha1) as HaC; lapply (segment_cauchy ? l u ? HaC) as Ha; lapply (sigma_cauchy ? H ? x ? Ha); [right; split; assumption] apply restric_uniform_convergence; assumption;] qed. -*) \ No newline at end of file diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma index 0a6d26112..4ba3ca3af 100644 --- a/helm/software/matita/contribs/dama/dama/supremum.ma +++ b/helm/software/matita/contribs/dama/dama/supremum.ma @@ -251,16 +251,18 @@ qed. lemma segment_ordered_set: ∀O:ordered_set.∀u,v:O.ordered_set. -intros (O u v); letin hos ≝ (half_segment_ordered_set (os_l O) u v); -constructor 1; [apply hos; | apply (dual_hos hos); | reflexivity] +intros (O u v); +apply half2full; apply (half_segment_ordered_set (os_l O) u v); qed. +(* notation < "hvbox({[a, break b]/})" non associative with precedence 90 for @{'h_segment_set $a $b}. notation > "hvbox({[a, break b]/})" non associative with precedence 90 for @{'h_segment_set $a $b}. interpretation "Half ordered set segment" 'h_segment_set a b = (half_segment_ordered_set _ a b). +*) notation < "hvbox({[a, break b]})" non associative with precedence 90 for @{'segment_set $a $b}. @@ -268,13 +270,41 @@ notation > "hvbox({[a, break b]})" non associative with precedence 90 for @{'segment_set $a $b}. interpretation "Ordered set segment" 'segment_set a b = (segment_ordered_set _ a b). + +definition hint_sequence: + ∀C:ordered_set. + sequence (hos_carr (os_l C)) → sequence (Type_of_ordered_set C). +intros;assumption; +qed. + +definition hint_sequence1: + ∀C:ordered_set. + sequence (hos_carr (os_r C)) → sequence (Type_of_ordered_set_dual C). +intros;assumption; +qed. + +definition hint_sequence2: + ∀C:ordered_set. + sequence (Type_of_ordered_set C) → sequence (hos_carr (os_l C)). +intros;assumption; +qed. + +definition hint_sequence3: + ∀C:ordered_set. + sequence (Type_of_ordered_set_dual C) → sequence (hos_carr (os_r C)). +intros;assumption; +qed. +coercion hint_sequence nocomposites. +coercion hint_sequence1 nocomposites. +coercion hint_sequence2 nocomposites. +coercion hint_sequence3 nocomposites. -(* Lemma 2.9 *) -lemma h_segment_preserves_supremum: - ∀O:half_ordered_set.∀l,u:O.∀a:sequence {[l,u]/}.∀x:{[l,u]/}. - increasing ? ⌊n,\fst (a n)⌋ ∧ - supremum ? ⌊n,\fst (a n)⌋ (\fst x) → uparrow ? a x. +(* Lemma 2.9 - non easily dualizable *) +lemma segment_preserves_supremum: + ∀O:ordered_set.∀l,u:O.∀a:sequence {[l,u]}.∀x:{[l,u]}. + ⌊n,\fst (a n)⌋ is_increasing ∧ + (\fst x) is_supremum ⌊n,\fst (a n)⌋ → a ↑ x. intros; split; cases H; clear H; [1: apply H1; |2: cases H2; split; clear H2; @@ -282,12 +312,17 @@ intros; split; cases H; clear H; |2: clear H; intro y0; apply (H3 (\fst y0));]] qed. -notation "'segment_preserves_supremum'" non associative with precedence 90 for @{'segment_preserves_supremum}. -notation "'segment_preserves_infimum'" non associative with precedence 90 for @{'segment_preserves_infimum}. - -interpretation "segment_preserves_supremum" 'segment_preserves_supremum = (h_segment_preserves_supremum (os_l _)). -interpretation "segment_preserves_infimum" 'segment_preserves_infimum = (h_segment_preserves_supremum (os_r _)). - +lemma segment_preserves_infimum: + ∀O:ordered_set.∀l,u:O.∀a:sequence {[l,u]}.∀x:{[l,u]}. + ⌊n,\fst (a n)⌋ is_decreasing ∧ + (\fst x) is_infimum ⌊n,\fst (a n)⌋ → a ↓ x. +intros; split; cases H; clear H; +[1: apply H1; +|2: cases H2; split; clear H2; + [1: apply H; + |2: clear H; intro y0; apply (H3 (\fst y0));]] +qed. + (* Definition 2.10 *) alias symbol "pi2" = "pair pi2". alias symbol "pi1" = "pair pi1".