From: Enrico Tassi Date: Wed, 7 Nov 2007 14:44:24 +0000 (+0000) Subject: reorganization of the whole story, the root dir contains the algebraic structure X-Git-Tag: make_still_working~5892 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fdcfbe23f5e11b1856ca6adbc78e5374b493d199;p=helm.git reorganization of the whole story, the root dir contains the algebraic structure --- diff --git a/helm/software/matita/dama/classical_pointfree/ordered_sets.ma b/helm/software/matita/dama/classical_pointfree/ordered_sets.ma new file mode 100644 index 000000000..18658cf7a --- /dev/null +++ b/helm/software/matita/dama/classical_pointfree/ordered_sets.ma @@ -0,0 +1,424 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/classical_pointwise/ordered_sets/". + +include "ordered_sets.ma". + +record is_dedekind_sigma_complete (O:ordered_set) : Type ≝ + { dsc_inf: ∀a:nat→O.∀m:O. is_lower_bound ? a m → ex ? (λs:O.is_inf O a s); + dsc_inf_proof_irrelevant: + ∀a:nat→O.∀m,m':O.∀p:is_lower_bound ? a m.∀p':is_lower_bound ? a m'. + (match dsc_inf a m p with [ ex_intro s _ ⇒ s ]) = + (match dsc_inf a m' p' with [ ex_intro s' _ ⇒ s' ]); + dsc_sup: ∀a:nat→O.∀m:O. is_upper_bound ? a m → ex ? (λs:O.is_sup O a s); + dsc_sup_proof_irrelevant: + ∀a:nat→O.∀m,m':O.∀p:is_upper_bound ? a m.∀p':is_upper_bound ? a m'. + (match dsc_sup a m p with [ ex_intro s _ ⇒ s ]) = + (match dsc_sup a m' p' with [ ex_intro s' _ ⇒ s' ]) + }. + +record dedekind_sigma_complete_ordered_set : Type ≝ + { dscos_ordered_set:> ordered_set; + dscos_dedekind_sigma_complete_properties:> + is_dedekind_sigma_complete dscos_ordered_set + }. + +definition inf: + ∀O:dedekind_sigma_complete_ordered_set. + bounded_below_sequence O → O. + intros; + elim + (dsc_inf O (dscos_dedekind_sigma_complete_properties O) b); + [ apply a + | apply (lower_bound ? b) + | apply lower_bound_is_lower_bound + ] +qed. + +lemma inf_is_inf: + ∀O:dedekind_sigma_complete_ordered_set. + ∀a:bounded_below_sequence O. + is_inf ? a (inf ? a). + intros; + unfold inf; + simplify; + elim (dsc_inf O (dscos_dedekind_sigma_complete_properties O) a +(lower_bound O a) (lower_bound_is_lower_bound O a)); + simplify; + assumption. +qed. + +lemma inf_proof_irrelevant: + ∀O:dedekind_sigma_complete_ordered_set. + ∀a,a':bounded_below_sequence O. + bbs_seq ? a = bbs_seq ? a' → + inf ? a = inf ? a'. + intros 3; + elim a 0; + elim a'; + simplify in H; + generalize in match i1; + clear i1; + rewrite > H; + intro; + simplify; + rewrite < (dsc_inf_proof_irrelevant O O f (ib_lower_bound ? f i) + (ib_lower_bound ? f i2) (ib_lower_bound_is_lower_bound ? f i) + (ib_lower_bound_is_lower_bound ? f i2)); + reflexivity. +qed. + +definition sup: + ∀O:dedekind_sigma_complete_ordered_set. + bounded_above_sequence O → O. + intros; + elim + (dsc_sup O (dscos_dedekind_sigma_complete_properties O) b); + [ apply a + | apply (upper_bound ? b) + | apply upper_bound_is_upper_bound + ]. +qed. + +lemma sup_is_sup: + ∀O:dedekind_sigma_complete_ordered_set. + ∀a:bounded_above_sequence O. + is_sup ? a (sup ? a). + intros; + unfold sup; + simplify; + elim (dsc_sup O (dscos_dedekind_sigma_complete_properties O) a +(upper_bound O a) (upper_bound_is_upper_bound O a)); + simplify; + assumption. +qed. + +lemma sup_proof_irrelevant: + ∀O:dedekind_sigma_complete_ordered_set. + ∀a,a':bounded_above_sequence O. + bas_seq ? a = bas_seq ? a' → + sup ? a = sup ? a'. + intros 3; + elim a 0; + elim a'; + simplify in H; + generalize in match i1; + clear i1; + rewrite > H; + intro; + simplify; + rewrite < (dsc_sup_proof_irrelevant O O f (ib_upper_bound ? f i2) + (ib_upper_bound ? f i) (ib_upper_bound_is_upper_bound ? f i2) + (ib_upper_bound_is_upper_bound ? f i)); + reflexivity. +qed. + +axiom daemon: False. + +theorem inf_le_sup: + ∀O:dedekind_sigma_complete_ordered_set. + ∀a:bounded_sequence O. inf ? a ≤ sup ? a. + intros (O'); + apply (or_transitive ? ? O' ? (a O)); + [ elim daemon (*apply (inf_lower_bound ? ? ? ? (inf_is_inf ? ? a))*) + | elim daemon (*apply (sup_upper_bound ? ? ? ? (sup_is_sup ? ? a))*) + ]. +qed. + +lemma inf_respects_le: + ∀O:dedekind_sigma_complete_ordered_set. + ∀a:bounded_below_sequence O.∀m:O. + is_upper_bound ? a m → inf ? a ≤ m. + intros (O'); + apply (or_transitive ? ? O' ? (sup ? (mk_bounded_sequence ? a ? ?))); + [ apply (bbs_is_bounded_below ? a) + | apply (mk_is_bounded_above ? ? m H) + | apply inf_le_sup + | apply + (sup_least_upper_bound ? ? ? + (sup_is_sup ? (mk_bounded_sequence O' a a + (mk_is_bounded_above O' a m H)))); + assumption + ]. +qed. + +definition is_sequentially_monotone ≝ + λO:ordered_set.λf:O→O. + ∀a:nat→O.∀p:is_increasing ? a. + is_increasing ? (λi.f (a i)). + +record is_order_continuous + (O:dedekind_sigma_complete_ordered_set) (f:O→O) : Prop +≝ + { ioc_is_sequentially_monotone: is_sequentially_monotone ? f; + ioc_is_upper_bound_f_sup: + ∀a:bounded_above_sequence O. + is_upper_bound ? (λi.f (a i)) (f (sup ? a)); + ioc_respects_sup: + ∀a:bounded_above_sequence O. + is_increasing ? a → + f (sup ? a) = + sup ? (mk_bounded_above_sequence ? (λi.f (a i)) + (mk_is_bounded_above ? ? (f (sup ? a)) + (ioc_is_upper_bound_f_sup a))); + ioc_is_lower_bound_f_inf: + ∀a:bounded_below_sequence O. + is_lower_bound ? (λi.f (a i)) (f (inf ? a)); + ioc_respects_inf: + ∀a:bounded_below_sequence O. + is_decreasing ? a → + f (inf ? a) = + inf ? (mk_bounded_below_sequence ? (λi.f (a i)) + (mk_is_bounded_below ? ? (f (inf ? a)) + (ioc_is_lower_bound_f_inf a))) + }. + +theorem tail_inf_increasing: + ∀O:dedekind_sigma_complete_ordered_set. + ∀a:bounded_below_sequence O. + let y ≝ λi.mk_bounded_below_sequence ? (λj.a (i+j)) ? in + let x ≝ λi.inf ? (y i) in + is_increasing ? x. + [ apply (mk_is_bounded_below ? ? (ib_lower_bound ? a a)); + simplify; + intro; + apply (ib_lower_bound_is_lower_bound ? a a) + | intros; + unfold is_increasing; + intro; + unfold x in ⊢ (? ? ? %); + apply (inf_greatest_lower_bound ? ? ? (inf_is_inf ? (y (S n)))); + change with (is_lower_bound ? (y (S n)) (inf ? (y n))); + unfold is_lower_bound; + intro; + generalize in match (inf_lower_bound ? ? ? (inf_is_inf ? (y n)) (S n1)); + (*CSC: coercion per FunClass inserita a mano*) + suppose (inf ? (y n) ≤ bbs_seq ? (y n) (S n1)) (H); + cut (bbs_seq ? (y n) (S n1) = bbs_seq ? (y (S n)) n1); + [ rewrite < Hcut; + assumption + | unfold y; + simplify; + autobatch paramodulation library + ] + ]. +qed. + +definition is_liminf: + ∀O:dedekind_sigma_complete_ordered_set. + bounded_below_sequence O → O → Prop. + intros; + apply + (is_sup ? (λi.inf ? (mk_bounded_below_sequence ? (λj.b (i+j)) ?)) t); + apply (mk_is_bounded_below ? ? (ib_lower_bound ? b b)); + simplify; + intros; + apply (ib_lower_bound_is_lower_bound ? b b). +qed. + +definition liminf: + ∀O:dedekind_sigma_complete_ordered_set. + bounded_sequence O → O. + intros; + apply + (sup ? + (mk_bounded_above_sequence ? + (λi.inf ? + (mk_bounded_below_sequence ? + (λj.b (i+j)) ?)) ?)); + [ apply (mk_is_bounded_below ? ? (ib_lower_bound ? b b)); + simplify; + intros; + apply (ib_lower_bound_is_lower_bound ? b b) + | apply (mk_is_bounded_above ? ? (ib_upper_bound ? b b)); + unfold is_upper_bound; + intro; + change with + (inf O + (mk_bounded_below_sequence O (\lambda j:nat.b (n+j)) + (mk_is_bounded_below O (\lambda j:nat.b (n+j)) (ib_lower_bound O b b) + (\lambda j:nat.ib_lower_bound_is_lower_bound O b b (n+j)))) +\leq ib_upper_bound O b b); + apply (inf_respects_le O); + simplify; + intro; + apply (ib_upper_bound_is_upper_bound ? b b) + ]. +qed. + + +definition reverse_dedekind_sigma_complete_ordered_set: + dedekind_sigma_complete_ordered_set → dedekind_sigma_complete_ordered_set. + intros; + apply mk_dedekind_sigma_complete_ordered_set; + [ apply (reverse_ordered_set d) + | elim daemon + (*apply mk_is_dedekind_sigma_complete; + [ intros; + elim (dsc_sup ? ? d a m) 0; + [ generalize in match H; clear H; + generalize in match m; clear m; + elim d; + simplify in a1; + simplify; + change in a1 with (Type_OF_ordered_set ? (reverse_ordered_set ? o)); + apply (ex_intro ? ? a1); + simplify in H1; + change in m with (Type_OF_ordered_set ? o); + apply (is_sup_to_reverse_is_inf ? ? ? ? H1) + | generalize in match H; clear H; + generalize in match m; clear m; + elim d; + simplify; + change in t with (Type_OF_ordered_set ? o); + simplify in t; + apply reverse_is_lower_bound_is_upper_bound; + assumption + ] + | apply is_sup_reverse_is_inf; + | apply m + | + ]*) + ]. +qed. + +definition reverse_bounded_sequence: + ∀O:dedekind_sigma_complete_ordered_set. + bounded_sequence O → + bounded_sequence (reverse_dedekind_sigma_complete_ordered_set O). + intros; + apply mk_bounded_sequence; + [ apply bs_seq; + unfold reverse_dedekind_sigma_complete_ordered_set; + simplify; + elim daemon + | elim daemon + | elim daemon + ]. +qed. + +definition limsup ≝ + λO:dedekind_sigma_complete_ordered_set. + λa:bounded_sequence O. + liminf (reverse_dedekind_sigma_complete_ordered_set O) + (reverse_bounded_sequence O a). + +notation "hvbox(〈a〉)" + non associative with precedence 45 +for @{ 'hide_everything_but $a }. + +interpretation "mk_bounded_above_sequence" 'hide_everything_but a += (cic:/matita/ordered_sets/bounded_above_sequence.ind#xpointer(1/1/1) _ _ a _). + +interpretation "mk_bounded_below_sequence" 'hide_everything_but a += (cic:/matita/ordered_sets/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _). + +theorem eq_f_sup_sup_f: + ∀O':dedekind_sigma_complete_ordered_set. + ∀f:O'→O'. ∀H:is_order_continuous ? f. + ∀a:bounded_above_sequence O'. + ∀p:is_increasing ? a. + f (sup ? a) = sup ? (mk_bounded_above_sequence ? (λi.f (a i)) ?). + [ apply (mk_is_bounded_above ? ? (f (sup ? a))); + apply ioc_is_upper_bound_f_sup; + assumption + | intros; + apply ioc_respects_sup; + assumption + ]. +qed. + +theorem eq_f_sup_sup_f': + ∀O':dedekind_sigma_complete_ordered_set. + ∀f:O'→O'. ∀H:is_order_continuous ? f. + ∀a:bounded_above_sequence O'. + ∀p:is_increasing ? a. + ∀p':is_bounded_above ? (λi.f (a i)). + f (sup ? a) = sup ? (mk_bounded_above_sequence ? (λi.f (a i)) p'). + intros; + rewrite > (eq_f_sup_sup_f ? f H a H1); + apply sup_proof_irrelevant; + reflexivity. +qed. + +theorem eq_f_liminf_sup_f_inf: + ∀O':dedekind_sigma_complete_ordered_set. + ∀f:O'→O'. ∀H:is_order_continuous ? f. + ∀a:bounded_sequence O'. + let p1 := ? in + f (liminf ? a) = + sup ? + (mk_bounded_above_sequence ? + (λi.f (inf ? + (mk_bounded_below_sequence ? + (λj.a (i+j)) + ?))) + p1). + [ apply (mk_is_bounded_below ? ? (ib_lower_bound ? a a)); + simplify; + intro; + apply (ib_lower_bound_is_lower_bound ? a a) + | apply (mk_is_bounded_above ? ? (f (sup ? a))); + unfold is_upper_bound; + intro; + apply (or_transitive ? ? O' ? (f (a n))); + [ generalize in match (ioc_is_lower_bound_f_inf ? ? H); + intro H1; + simplify in H1; + rewrite > (plus_n_O n) in ⊢ (? ? ? (? (? ? ? %))); + apply (H1 (mk_bounded_below_sequence O' (\lambda j:nat.a (n+j)) +(mk_is_bounded_below O' (\lambda j:nat.a (n+j)) (ib_lower_bound O' a a) + (\lambda j:nat.ib_lower_bound_is_lower_bound O' a a (n+j)))) O); + | elim daemon (*apply (ioc_is_upper_bound_f_sup ? ? ? H)*) + ] + | intros; + unfold liminf; + clearbody p1; + generalize in match (\lambda n:nat +.inf_respects_le O' + (mk_bounded_below_sequence O' (\lambda j:nat.a (plus n j)) + (mk_is_bounded_below O' (\lambda j:nat.a (plus n j)) + (ib_lower_bound O' a a) + (\lambda j:nat.ib_lower_bound_is_lower_bound O' a a (plus n j)))) + (ib_upper_bound O' a a) + (\lambda n1:nat.ib_upper_bound_is_upper_bound O' a a (plus n n1))); + intro p2; + apply (eq_f_sup_sup_f' ? f H (mk_bounded_above_sequence O' +(\lambda i:nat + .inf O' + (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j)) + (mk_is_bounded_below O' (\lambda j:nat.a (plus i j)) + (ib_lower_bound O' a a) + (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n))))) +(mk_is_bounded_above O' + (\lambda i:nat + .inf O' + (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j)) + (mk_is_bounded_below O' (\lambda j:nat.a (plus i j)) + (ib_lower_bound O' a a) + (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n))))) + (ib_upper_bound O' a a) p2))); + unfold bas_seq; + change with + (is_increasing ? (\lambda i:nat +.inf O' + (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j)) + (mk_is_bounded_below O' (\lambda j:nat.a (plus i j)) + (ib_lower_bound O' a a) + (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n)))))); + apply tail_inf_increasing + ]. +qed. + diff --git a/helm/software/matita/dama/classical_pointfree/ordered_sets2.ma b/helm/software/matita/dama/classical_pointfree/ordered_sets2.ma new file mode 100644 index 000000000..dafa0df4f --- /dev/null +++ b/helm/software/matita/dama/classical_pointfree/ordered_sets2.ma @@ -0,0 +1,127 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/classical_pointfree/ordered_sets2". + +include "classical_pointfree/ordered_sets.ma". + +theorem le_f_inf_inf_f: + ∀O':dedekind_sigma_complete_ordered_set. + ∀f:O'→O'. ∀H:is_order_continuous ? f. + ∀a:bounded_below_sequence O'. + let p := ? in + f (inf ? a) ≤ inf ? (mk_bounded_below_sequence ? (λi. f (a i)) p). + [ apply mk_is_bounded_below; + [2: apply ioc_is_lower_bound_f_inf; + assumption + | skip + ] + | intros; + clearbody p; + apply (inf_greatest_lower_bound ? ? ? (inf_is_inf ? ?)); + simplify; + intro; + letin b := (λi.match i with [ O ⇒ inf ? a | S _ ⇒ a n]); + change with (f (b O) ≤ f (b (S O))); + apply (ioc_is_sequentially_monotone ? ? H); + simplify; + clear b; + intro; + elim n1; simplify; + [ apply (inf_lower_bound ? ? ? (inf_is_inf ? ?)); + | apply (or_reflexive O' ? (dscos_ordered_set O')) + ] + ]. +qed. + +theorem le_to_le_sup_sup: + ∀O':dedekind_sigma_complete_ordered_set. + ∀a,b:bounded_above_sequence O'. + (∀i.a i ≤ b i) → sup ? a ≤ sup ? b. + intros; + apply (sup_least_upper_bound ? ? ? (sup_is_sup ? a)); + unfold; + intro; + apply (or_transitive ? ? O'); + [2: apply H + | skip + | apply (sup_upper_bound ? ? ? (sup_is_sup ? b)) + ]. +qed. + +interpretation "mk_bounded_sequence" 'hide_everything_but a += (cic:/matita/ordered_sets/bounded_sequence.ind#xpointer(1/1/1) _ _ a _ _). + +lemma reduce_bas_seq: + ∀O:ordered_set.∀a:nat→O.∀p.∀i. + bas_seq ? (mk_bounded_above_sequence ? a p) i = a i. + intros; + reflexivity. +qed. + +(*lemma reduce_bbs_seq: + ∀C.∀O:ordered_set C.∀a:nat→O.∀p.∀i. + bbs_seq ? ? (mk_bounded_below_sequence ? ? a p) i = a i. + intros; + reflexivity. +qed.*) + +axiom inf_extensional: + ∀O:dedekind_sigma_complete_ordered_set. + ∀a,b:bounded_below_sequence O. + (∀i.a i = b i) → inf ? a = inf O b. + +lemma eq_to_le: ∀O:ordered_set.∀x,y:O.x=y → x ≤ y. + intros; + rewrite > H; + apply (or_reflexive ? ? O). +qed. + +theorem fatou: + ∀O':dedekind_sigma_complete_ordered_set. + ∀f:O'→O'. ∀H:is_order_continuous ? f. + ∀a:bounded_sequence O'. + let pb := ? in + let pa := ? in + f (liminf ? a) ≤ liminf ? (mk_bounded_sequence ? (λi. f (a i)) pb pa). + [ letin bas ≝ (bounded_above_sequence_of_bounded_sequence ? a); + apply mk_is_bounded_above; + [2: apply (ioc_is_upper_bound_f_sup ? ? H bas) + | skip + ] + | letin bbs ≝ (bounded_below_sequence_of_bounded_sequence ? a); + apply mk_is_bounded_below; + [2: apply (ioc_is_lower_bound_f_inf ? ? H bbs) + | skip + ] + | intros; + rewrite > eq_f_liminf_sup_f_inf in ⊢ (? ? % ?); + [ unfold liminf; + apply le_to_le_sup_sup; + intro; + rewrite > reduce_bas_seq; + rewrite > reduce_bas_seq; + apply (or_transitive ? ? O'); + [2: apply le_f_inf_inf_f; + assumption + | skip + | apply eq_to_le; + apply inf_extensional; + intro; + reflexivity + ] + | assumption + ] + ]. +qed. diff --git a/helm/software/matita/dama/classical_pointwise/sets.ma b/helm/software/matita/dama/classical_pointwise/sets.ma new file mode 100644 index 000000000..ec6a1c774 --- /dev/null +++ b/helm/software/matita/dama/classical_pointwise/sets.ma @@ -0,0 +1,102 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/sets/". + +include "nat/nat.ma". + +definition set ≝ λX:Type.X → Prop. + +definition member_of : ∀X.set X → X → Prop≝ λX.λA:set X.λx.A x. + +notation "hvbox(x break ∈ A)" with precedence 60 +for @{ 'member_of $x $A }. + +interpretation "Member of" 'member_of x A = + (cic:/matita/sets/member_of.con _ A x). + +notation "hvbox(x break ∉ A)" with precedence 60 +for @{ 'not_member_of $x $A }. + +interpretation "Not member of" 'not_member_of x A = + (cic:/matita/logic/connectives/Not.con + (cic:/matita/sets/member_of.con _ A x)). + +definition emptyset : ∀X.set X ≝ λX:Type.λx:X.False. + +notation "∅︀" with precedence 100 for @{ 'emptyset }. + +interpretation "Emptyset" 'emptyset = + (cic:/matita/sets/emptyset.con _). + +definition subset: ∀X. set X → set X → Prop≝ λX.λA,B:set X.∀x. x ∈ A → x ∈ B. + +notation "hvbox(A break ⊆ B)" with precedence 60 +for @{ 'subset $A $B }. + +interpretation "Subset" 'subset A B = + (cic:/matita/sets/subset.con _ A B). + +definition intersection: ∀X. set X → set X → set X ≝ + λX.λA,B:set X.λx. x ∈ A ∧ x ∈ B. + +notation "hvbox(A break ∩ B)" with precedence 70 +for @{ 'intersection $A $B }. + +interpretation "Intersection" 'intersection A B = + (cic:/matita/sets/intersection.con _ A B). + +definition union: ∀X. set X → set X → set X ≝ λX.λA,B:set X.λx. x ∈ A ∨ x ∈ B. + +notation "hvbox(A break ∪ B)" with precedence 65 +for @{ 'union $A $B }. + +interpretation "Union" 'union A B = + (cic:/matita/sets/union.con _ A B). + +definition seq ≝ λX:Type.nat → X. + +definition nth ≝ λX.λA:seq X.λi.A i. + +notation "hvbox(A \sub i)" with precedence 100 +for @{ 'nth $A $i }. + +interpretation "nth" 'nth A i = + (cic:/matita/sets/nth.con _ A i). + +definition countable_union: ∀X. seq (set X) → set X ≝ + λX.λA:seq (set X).λx.∃j.x ∈ A \sub j. + +notation "∪ \sub (ident i opt (: ty)) B" with precedence 65 +for @{ 'big_union ${default @{(λ${ident i}:$ty.$B)} @{(λ${ident i}.$B)}}}. + +interpretation "countable_union" 'big_union η.t = + (cic:/matita/sets/countable_union.con _ t). + +definition complement: ∀X. set X \to set X ≝ λX.λA:set X.λx. x ∉ A. + +notation "A \sup 'c'" with precedence 100 +for @{ 'complement $A }. + +interpretation "Complement" 'complement A = + (cic:/matita/sets/complement.con _ A). + +definition inverse_image: ∀X,Y.∀f: X → Y.set Y → set X ≝ + λX,Y,f,B,x. f x ∈ B. + +notation "hvbox(f \sup (-1))" with precedence 100 +for @{ 'finverse $f }. + +interpretation "Inverse image" 'finverse f = + (cic:/matita/sets/inverse_image.con _ _ f). \ No newline at end of file diff --git a/helm/software/matita/dama/classical_pointwise/sigma_algebra.ma b/helm/software/matita/dama/classical_pointwise/sigma_algebra.ma new file mode 100644 index 000000000..21db34e38 --- /dev/null +++ b/helm/software/matita/dama/classical_pointwise/sigma_algebra.ma @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/sigma_algebra/". + +include "classical_pointwise/topology.ma". + +record is_sigma_algebra (X:Type) (A: set X) (M: set (set X)) : Prop ≝ + { siga_subset: ∀B.B ∈ M → B ⊆ A; + siga_full: A ∈ M; + siga_compl: ∀B.B ∈ M → B \sup c ∈ M; + siga_enumerable_union: + ∀B:seq (set X).(∀i.(B \sub i) ∈ M) → (∪ \sub i B \sub i) ∈ M + }. + +record sigma_algebra : Type ≝ + { siga_carrier:> Type; + siga_domain:> set siga_carrier; + M: set (set siga_carrier); + siga_is_sigma_algebra:> is_sigma_algebra ? siga_domain M + }. + +(*definition is_measurable_map ≝ + λX:sigma_algebra.λY:topological_space.λf:X → Y. + ∀V. V ∈ O Y → f \sup -1 V ∈ M X.*) +definition is_measurable_map ≝ + λX:sigma_algebra.λY:topological_space.λf:X → Y. + ∀V. V ∈ O Y → inverse_image ? ? f V ∈ M X. + diff --git a/helm/software/matita/dama/classical_pointwise/topology.ma b/helm/software/matita/dama/classical_pointwise/topology.ma new file mode 100644 index 000000000..c5ba9bbd6 --- /dev/null +++ b/helm/software/matita/dama/classical_pointwise/topology.ma @@ -0,0 +1,45 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/topology/". + +include "classical_pointwise/sets.ma". + +record is_topology (X) (A: set X) (O: set (set X)) : Prop ≝ + { top_subset: ∀B. B ∈ O → B ⊆ A; + top_empty: ∅︀ ∈ O; + top_full: A ∈ O; + top_intersection: ∀B,C. B ∈ O → C ∈ O → B ∩ C ∈ O; + top_countable_union: + ∀B.(∀i.(B \sub i) ∈ O) → (∪ \sub i (B \sub i)) ∈ O + }. + +record topological_space : Type ≝ + { top_carrier:> Type; + top_domain:> set top_carrier; + O: set (set top_carrier); + top_is_topological_space:> is_topology ? top_domain O + }. + +(*definition is_continuous_map ≝ + λX,Y: topological_space.λf: X → Y. + ∀V. V ∈ O Y → (f \sup -1) V ∈ O X.*) +definition is_continuous_map ≝ + λX,Y: topological_space.λf: X → Y. + ∀V. V ∈ O Y → inverse_image ? ? f V ∈ O X. + +record continuous_map (X,Y: topological_space) : Type ≝ + { cm_f:> X → Y; + cm_is_continuous_map: is_continuous_map ? ? cm_f + }. diff --git a/helm/software/matita/dama/ordered_groups.ma b/helm/software/matita/dama/ordered_groups.ma index a9912d43f..10e8f189a 100644 --- a/helm/software/matita/dama/ordered_groups.ma +++ b/helm/software/matita/dama/ordered_groups.ma @@ -15,7 +15,7 @@ set "baseuri" "cic:/matita/ordered_groups/". include "groups.ma". -include "ordered_sets2.ma". +include "ordered_sets.ma". record pre_ordered_abelian_group : Type ≝ { og_abelian_group:> abelian_group; diff --git a/helm/software/matita/dama/ordered_sets.ma b/helm/software/matita/dama/ordered_sets.ma index 62b934865..dcae29e18 100644 --- a/helm/software/matita/dama/ordered_sets.ma +++ b/helm/software/matita/dama/ordered_sets.ma @@ -135,247 +135,10 @@ lemma upper_bound_is_upper_bound: apply ib_upper_bound_is_upper_bound. qed. -record is_dedekind_sigma_complete (O:ordered_set) : Type ≝ - { dsc_inf: ∀a:nat→O.∀m:O. is_lower_bound ? a m → ex ? (λs:O.is_inf O a s); - dsc_inf_proof_irrelevant: - ∀a:nat→O.∀m,m':O.∀p:is_lower_bound ? a m.∀p':is_lower_bound ? a m'. - (match dsc_inf a m p with [ ex_intro s _ ⇒ s ]) = - (match dsc_inf a m' p' with [ ex_intro s' _ ⇒ s' ]); - dsc_sup: ∀a:nat→O.∀m:O. is_upper_bound ? a m → ex ? (λs:O.is_sup O a s); - dsc_sup_proof_irrelevant: - ∀a:nat→O.∀m,m':O.∀p:is_upper_bound ? a m.∀p':is_upper_bound ? a m'. - (match dsc_sup a m p with [ ex_intro s _ ⇒ s ]) = - (match dsc_sup a m' p' with [ ex_intro s' _ ⇒ s' ]) - }. - -record dedekind_sigma_complete_ordered_set : Type ≝ - { dscos_ordered_set:> ordered_set; - dscos_dedekind_sigma_complete_properties:> - is_dedekind_sigma_complete dscos_ordered_set - }. - -definition inf: - ∀O:dedekind_sigma_complete_ordered_set. - bounded_below_sequence O → O. - intros; - elim - (dsc_inf O (dscos_dedekind_sigma_complete_properties O) b); - [ apply a - | apply (lower_bound ? b) - | apply lower_bound_is_lower_bound - ] -qed. - -lemma inf_is_inf: - ∀O:dedekind_sigma_complete_ordered_set. - ∀a:bounded_below_sequence O. - is_inf ? a (inf ? a). - intros; - unfold inf; - simplify; - elim (dsc_inf O (dscos_dedekind_sigma_complete_properties O) a -(lower_bound O a) (lower_bound_is_lower_bound O a)); - simplify; - assumption. -qed. - -lemma inf_proof_irrelevant: - ∀O:dedekind_sigma_complete_ordered_set. - ∀a,a':bounded_below_sequence O. - bbs_seq ? a = bbs_seq ? a' → - inf ? a = inf ? a'. - intros 3; - elim a 0; - elim a'; - simplify in H; - generalize in match i1; - clear i1; - rewrite > H; - intro; - simplify; - rewrite < (dsc_inf_proof_irrelevant O O f (ib_lower_bound ? f i) - (ib_lower_bound ? f i2) (ib_lower_bound_is_lower_bound ? f i) - (ib_lower_bound_is_lower_bound ? f i2)); - reflexivity. -qed. - -definition sup: - ∀O:dedekind_sigma_complete_ordered_set. - bounded_above_sequence O → O. - intros; - elim - (dsc_sup O (dscos_dedekind_sigma_complete_properties O) b); - [ apply a - | apply (upper_bound ? b) - | apply upper_bound_is_upper_bound - ]. -qed. - -lemma sup_is_sup: - ∀O:dedekind_sigma_complete_ordered_set. - ∀a:bounded_above_sequence O. - is_sup ? a (sup ? a). - intros; - unfold sup; - simplify; - elim (dsc_sup O (dscos_dedekind_sigma_complete_properties O) a -(upper_bound O a) (upper_bound_is_upper_bound O a)); - simplify; - assumption. -qed. - -lemma sup_proof_irrelevant: - ∀O:dedekind_sigma_complete_ordered_set. - ∀a,a':bounded_above_sequence O. - bas_seq ? a = bas_seq ? a' → - sup ? a = sup ? a'. - intros 3; - elim a 0; - elim a'; - simplify in H; - generalize in match i1; - clear i1; - rewrite > H; - intro; - simplify; - rewrite < (dsc_sup_proof_irrelevant O O f (ib_upper_bound ? f i2) - (ib_upper_bound ? f i) (ib_upper_bound_is_upper_bound ? f i2) - (ib_upper_bound_is_upper_bound ? f i)); - reflexivity. -qed. - -axiom daemon: False. - -theorem inf_le_sup: - ∀O:dedekind_sigma_complete_ordered_set. - ∀a:bounded_sequence O. inf ? a ≤ sup ? a. - intros (O'); - apply (or_transitive ? ? O' ? (a O)); - [ elim daemon (*apply (inf_lower_bound ? ? ? ? (inf_is_inf ? ? a))*) - | elim daemon (*apply (sup_upper_bound ? ? ? ? (sup_is_sup ? ? a))*) - ]. -qed. - -lemma inf_respects_le: - ∀O:dedekind_sigma_complete_ordered_set. - ∀a:bounded_below_sequence O.∀m:O. - is_upper_bound ? a m → inf ? a ≤ m. - intros (O'); - apply (or_transitive ? ? O' ? (sup ? (mk_bounded_sequence ? a ? ?))); - [ apply (bbs_is_bounded_below ? a) - | apply (mk_is_bounded_above ? ? m H) - | apply inf_le_sup - | apply - (sup_least_upper_bound ? ? ? - (sup_is_sup ? (mk_bounded_sequence O' a a - (mk_is_bounded_above O' a m H)))); - assumption - ]. -qed. - -definition is_sequentially_monotone ≝ - λO:ordered_set.λf:O→O. - ∀a:nat→O.∀p:is_increasing ? a. - is_increasing ? (λi.f (a i)). - -record is_order_continuous - (O:dedekind_sigma_complete_ordered_set) (f:O→O) : Prop -≝ - { ioc_is_sequentially_monotone: is_sequentially_monotone ? f; - ioc_is_upper_bound_f_sup: - ∀a:bounded_above_sequence O. - is_upper_bound ? (λi.f (a i)) (f (sup ? a)); - ioc_respects_sup: - ∀a:bounded_above_sequence O. - is_increasing ? a → - f (sup ? a) = - sup ? (mk_bounded_above_sequence ? (λi.f (a i)) - (mk_is_bounded_above ? ? (f (sup ? a)) - (ioc_is_upper_bound_f_sup a))); - ioc_is_lower_bound_f_inf: - ∀a:bounded_below_sequence O. - is_lower_bound ? (λi.f (a i)) (f (inf ? a)); - ioc_respects_inf: - ∀a:bounded_below_sequence O. - is_decreasing ? a → - f (inf ? a) = - inf ? (mk_bounded_below_sequence ? (λi.f (a i)) - (mk_is_bounded_below ? ? (f (inf ? a)) - (ioc_is_lower_bound_f_inf a))) - }. - -theorem tail_inf_increasing: - ∀O:dedekind_sigma_complete_ordered_set. - ∀a:bounded_below_sequence O. - let y ≝ λi.mk_bounded_below_sequence ? (λj.a (i+j)) ? in - let x ≝ λi.inf ? (y i) in - is_increasing ? x. - [ apply (mk_is_bounded_below ? ? (ib_lower_bound ? a a)); - simplify; - intro; - apply (ib_lower_bound_is_lower_bound ? a a) - | intros; - unfold is_increasing; - intro; - unfold x in ⊢ (? ? ? %); - apply (inf_greatest_lower_bound ? ? ? (inf_is_inf ? (y (S n)))); - change with (is_lower_bound ? (y (S n)) (inf ? (y n))); - unfold is_lower_bound; - intro; - generalize in match (inf_lower_bound ? ? ? (inf_is_inf ? (y n)) (S n1)); - (*CSC: coercion per FunClass inserita a mano*) - suppose (inf ? (y n) ≤ bbs_seq ? (y n) (S n1)) (H); - cut (bbs_seq ? (y n) (S n1) = bbs_seq ? (y (S n)) n1); - [ rewrite < Hcut; - assumption - | unfold y; - simplify; - autobatch paramodulation library - ] - ]. -qed. - -definition is_liminf: - ∀O:dedekind_sigma_complete_ordered_set. - bounded_below_sequence O → O → Prop. - intros; - apply - (is_sup ? (λi.inf ? (mk_bounded_below_sequence ? (λj.b (i+j)) ?)) t); - apply (mk_is_bounded_below ? ? (ib_lower_bound ? b b)); - simplify; - intros; - apply (ib_lower_bound_is_lower_bound ? b b). -qed. +definition lt ≝ λO:ordered_set.λa,b:O.a ≤ b ∧ a ≠ b. -definition liminf: - ∀O:dedekind_sigma_complete_ordered_set. - bounded_sequence O → O. - intros; - apply - (sup ? - (mk_bounded_above_sequence ? - (λi.inf ? - (mk_bounded_below_sequence ? - (λj.b (i+j)) ?)) ?)); - [ apply (mk_is_bounded_below ? ? (ib_lower_bound ? b b)); - simplify; - intros; - apply (ib_lower_bound_is_lower_bound ? b b) - | apply (mk_is_bounded_above ? ? (ib_upper_bound ? b b)); - unfold is_upper_bound; - intro; - change with - (inf O - (mk_bounded_below_sequence O (\lambda j:nat.b (n+j)) - (mk_is_bounded_below O (\lambda j:nat.b (n+j)) (ib_lower_bound O b b) - (\lambda j:nat.ib_lower_bound_is_lower_bound O b b (n+j)))) -\leq ib_upper_bound O b b); - apply (inf_respects_le O); - simplify; - intro; - apply (ib_upper_bound_is_upper_bound ? b b) - ]. -qed. +interpretation "Ordered set lt" 'lt a b = + (cic:/matita/ordered_sets/lt.con _ a b). definition reverse_ordered_set: ordered_set → ordered_set. intros; @@ -522,174 +285,7 @@ lemma reverse_is_inf_to_is_sup: ]. qed. - -definition reverse_dedekind_sigma_complete_ordered_set: - dedekind_sigma_complete_ordered_set → dedekind_sigma_complete_ordered_set. - intros; - apply mk_dedekind_sigma_complete_ordered_set; - [ apply (reverse_ordered_set d) - | elim daemon - (*apply mk_is_dedekind_sigma_complete; - [ intros; - elim (dsc_sup ? ? d a m) 0; - [ generalize in match H; clear H; - generalize in match m; clear m; - elim d; - simplify in a1; - simplify; - change in a1 with (Type_OF_ordered_set ? (reverse_ordered_set ? o)); - apply (ex_intro ? ? a1); - simplify in H1; - change in m with (Type_OF_ordered_set ? o); - apply (is_sup_to_reverse_is_inf ? ? ? ? H1) - | generalize in match H; clear H; - generalize in match m; clear m; - elim d; - simplify; - change in t with (Type_OF_ordered_set ? o); - simplify in t; - apply reverse_is_lower_bound_is_upper_bound; - assumption - ] - | apply is_sup_reverse_is_inf; - | apply m - | - ]*) - ]. -qed. - -definition reverse_bounded_sequence: - ∀O:dedekind_sigma_complete_ordered_set. - bounded_sequence O → - bounded_sequence (reverse_dedekind_sigma_complete_ordered_set O). - intros; - apply mk_bounded_sequence; - [ apply bs_seq; - unfold reverse_dedekind_sigma_complete_ordered_set; - simplify; - elim daemon - | elim daemon - | elim daemon - ]. -qed. - -definition limsup ≝ - λO:dedekind_sigma_complete_ordered_set. - λa:bounded_sequence O. - liminf (reverse_dedekind_sigma_complete_ordered_set O) - (reverse_bounded_sequence O a). - -notation "hvbox(〈a〉)" - non associative with precedence 45 -for @{ 'hide_everything_but $a }. - -interpretation "mk_bounded_above_sequence" 'hide_everything_but a -= (cic:/matita/ordered_sets/bounded_above_sequence.ind#xpointer(1/1/1) _ _ a _). - -interpretation "mk_bounded_below_sequence" 'hide_everything_but a -= (cic:/matita/ordered_sets/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _). - -theorem eq_f_sup_sup_f: - ∀O':dedekind_sigma_complete_ordered_set. - ∀f:O'→O'. ∀H:is_order_continuous ? f. - ∀a:bounded_above_sequence O'. - ∀p:is_increasing ? a. - f (sup ? a) = sup ? (mk_bounded_above_sequence ? (λi.f (a i)) ?). - [ apply (mk_is_bounded_above ? ? (f (sup ? a))); - apply ioc_is_upper_bound_f_sup; - assumption - | intros; - apply ioc_respects_sup; - assumption - ]. -qed. - -theorem eq_f_sup_sup_f': - ∀O':dedekind_sigma_complete_ordered_set. - ∀f:O'→O'. ∀H:is_order_continuous ? f. - ∀a:bounded_above_sequence O'. - ∀p:is_increasing ? a. - ∀p':is_bounded_above ? (λi.f (a i)). - f (sup ? a) = sup ? (mk_bounded_above_sequence ? (λi.f (a i)) p'). - intros; - rewrite > (eq_f_sup_sup_f ? f H a H1); - apply sup_proof_irrelevant; - reflexivity. -qed. - -theorem eq_f_liminf_sup_f_inf: - ∀O':dedekind_sigma_complete_ordered_set. - ∀f:O'→O'. ∀H:is_order_continuous ? f. - ∀a:bounded_sequence O'. - let p1 := ? in - f (liminf ? a) = - sup ? - (mk_bounded_above_sequence ? - (λi.f (inf ? - (mk_bounded_below_sequence ? - (λj.a (i+j)) - ?))) - p1). - [ apply (mk_is_bounded_below ? ? (ib_lower_bound ? a a)); - simplify; - intro; - apply (ib_lower_bound_is_lower_bound ? a a) - | apply (mk_is_bounded_above ? ? (f (sup ? a))); - unfold is_upper_bound; - intro; - apply (or_transitive ? ? O' ? (f (a n))); - [ generalize in match (ioc_is_lower_bound_f_inf ? ? H); - intro H1; - simplify in H1; - rewrite > (plus_n_O n) in ⊢ (? ? ? (? (? ? ? %))); - apply (H1 (mk_bounded_below_sequence O' (\lambda j:nat.a (n+j)) -(mk_is_bounded_below O' (\lambda j:nat.a (n+j)) (ib_lower_bound O' a a) - (\lambda j:nat.ib_lower_bound_is_lower_bound O' a a (n+j)))) O); - | elim daemon (*apply (ioc_is_upper_bound_f_sup ? ? ? H)*) - ] - | intros; - unfold liminf; - clearbody p1; - generalize in match (\lambda n:nat -.inf_respects_le O' - (mk_bounded_below_sequence O' (\lambda j:nat.a (plus n j)) - (mk_is_bounded_below O' (\lambda j:nat.a (plus n j)) - (ib_lower_bound O' a a) - (\lambda j:nat.ib_lower_bound_is_lower_bound O' a a (plus n j)))) - (ib_upper_bound O' a a) - (\lambda n1:nat.ib_upper_bound_is_upper_bound O' a a (plus n n1))); - intro p2; - apply (eq_f_sup_sup_f' ? f H (mk_bounded_above_sequence O' -(\lambda i:nat - .inf O' - (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j)) - (mk_is_bounded_below O' (\lambda j:nat.a (plus i j)) - (ib_lower_bound O' a a) - (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n))))) -(mk_is_bounded_above O' - (\lambda i:nat - .inf O' - (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j)) - (mk_is_bounded_below O' (\lambda j:nat.a (plus i j)) - (ib_lower_bound O' a a) - (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n))))) - (ib_upper_bound O' a a) p2))); - unfold bas_seq; - change with - (is_increasing ? (\lambda i:nat -.inf O' - (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j)) - (mk_is_bounded_below O' (\lambda j:nat.a (plus i j)) - (ib_lower_bound O' a a) - (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n)))))); - apply tail_inf_increasing - ]. -qed. - - - - -definition lt ≝ λO:ordered_set.λa,b:O.a ≤ b ∧ a ≠ b. - -interpretation "Ordered set lt" 'lt a b = - (cic:/matita/ordered_sets/lt.con _ a b). +record cotransitively_ordered_set: Type := + { cos_ordered_set :> ordered_set; + cos_cotransitive: cotransitive ? (os_le cos_ordered_set) + }. diff --git a/helm/software/matita/dama/ordered_sets2.ma b/helm/software/matita/dama/ordered_sets2.ma deleted file mode 100644 index a8050ec21..000000000 --- a/helm/software/matita/dama/ordered_sets2.ma +++ /dev/null @@ -1,132 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -set "baseuri" "cic:/matita/ordered_sets2". - -include "ordered_sets.ma". - -theorem le_f_inf_inf_f: - ∀O':dedekind_sigma_complete_ordered_set. - ∀f:O'→O'. ∀H:is_order_continuous ? f. - ∀a:bounded_below_sequence O'. - let p := ? in - f (inf ? a) ≤ inf ? (mk_bounded_below_sequence ? (λi. f (a i)) p). - [ apply mk_is_bounded_below; - [2: apply ioc_is_lower_bound_f_inf; - assumption - | skip - ] - | intros; - clearbody p; - apply (inf_greatest_lower_bound ? ? ? (inf_is_inf ? ?)); - simplify; - intro; - letin b := (λi.match i with [ O ⇒ inf ? a | S _ ⇒ a n]); - change with (f (b O) ≤ f (b (S O))); - apply (ioc_is_sequentially_monotone ? ? H); - simplify; - clear b; - intro; - elim n1; simplify; - [ apply (inf_lower_bound ? ? ? (inf_is_inf ? ?)); - | apply (or_reflexive O' ? (dscos_ordered_set O')) - ] - ]. -qed. - -theorem le_to_le_sup_sup: - ∀O':dedekind_sigma_complete_ordered_set. - ∀a,b:bounded_above_sequence O'. - (∀i.a i ≤ b i) → sup ? a ≤ sup ? b. - intros; - apply (sup_least_upper_bound ? ? ? (sup_is_sup ? a)); - unfold; - intro; - apply (or_transitive ? ? O'); - [2: apply H - | skip - | apply (sup_upper_bound ? ? ? (sup_is_sup ? b)) - ]. -qed. - -interpretation "mk_bounded_sequence" 'hide_everything_but a -= (cic:/matita/ordered_sets/bounded_sequence.ind#xpointer(1/1/1) _ _ a _ _). - -lemma reduce_bas_seq: - ∀O:ordered_set.∀a:nat→O.∀p.∀i. - bas_seq ? (mk_bounded_above_sequence ? a p) i = a i. - intros; - reflexivity. -qed. - -(*lemma reduce_bbs_seq: - ∀C.∀O:ordered_set C.∀a:nat→O.∀p.∀i. - bbs_seq ? ? (mk_bounded_below_sequence ? ? a p) i = a i. - intros; - reflexivity. -qed.*) - -axiom inf_extensional: - ∀O:dedekind_sigma_complete_ordered_set. - ∀a,b:bounded_below_sequence O. - (∀i.a i = b i) → inf ? a = inf O b. - -lemma eq_to_le: ∀O:ordered_set.∀x,y:O.x=y → x ≤ y. - intros; - rewrite > H; - apply (or_reflexive ? ? O). -qed. - -theorem fatou: - ∀O':dedekind_sigma_complete_ordered_set. - ∀f:O'→O'. ∀H:is_order_continuous ? f. - ∀a:bounded_sequence O'. - let pb := ? in - let pa := ? in - f (liminf ? a) ≤ liminf ? (mk_bounded_sequence ? (λi. f (a i)) pb pa). - [ letin bas ≝ (bounded_above_sequence_of_bounded_sequence ? a); - apply mk_is_bounded_above; - [2: apply (ioc_is_upper_bound_f_sup ? ? H bas) - | skip - ] - | letin bbs ≝ (bounded_below_sequence_of_bounded_sequence ? a); - apply mk_is_bounded_below; - [2: apply (ioc_is_lower_bound_f_inf ? ? H bbs) - | skip - ] - | intros; - rewrite > eq_f_liminf_sup_f_inf in ⊢ (? ? % ?); - [ unfold liminf; - apply le_to_le_sup_sup; - intro; - rewrite > reduce_bas_seq; - rewrite > reduce_bas_seq; - apply (or_transitive ? ? O'); - [2: apply le_f_inf_inf_f; - assumption - | skip - | apply eq_to_le; - apply inf_extensional; - intro; - reflexivity - ] - | assumption - ] - ]. -qed. - -record cotransitively_ordered_set: Type := - { cos_ordered_set :> ordered_set; - cos_cotransitive: cotransitive ? (os_le cos_ordered_set) - }. diff --git a/helm/software/matita/dama/sets.ma b/helm/software/matita/dama/sets.ma deleted file mode 100644 index ec6a1c774..000000000 --- a/helm/software/matita/dama/sets.ma +++ /dev/null @@ -1,102 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -set "baseuri" "cic:/matita/sets/". - -include "nat/nat.ma". - -definition set ≝ λX:Type.X → Prop. - -definition member_of : ∀X.set X → X → Prop≝ λX.λA:set X.λx.A x. - -notation "hvbox(x break ∈ A)" with precedence 60 -for @{ 'member_of $x $A }. - -interpretation "Member of" 'member_of x A = - (cic:/matita/sets/member_of.con _ A x). - -notation "hvbox(x break ∉ A)" with precedence 60 -for @{ 'not_member_of $x $A }. - -interpretation "Not member of" 'not_member_of x A = - (cic:/matita/logic/connectives/Not.con - (cic:/matita/sets/member_of.con _ A x)). - -definition emptyset : ∀X.set X ≝ λX:Type.λx:X.False. - -notation "∅︀" with precedence 100 for @{ 'emptyset }. - -interpretation "Emptyset" 'emptyset = - (cic:/matita/sets/emptyset.con _). - -definition subset: ∀X. set X → set X → Prop≝ λX.λA,B:set X.∀x. x ∈ A → x ∈ B. - -notation "hvbox(A break ⊆ B)" with precedence 60 -for @{ 'subset $A $B }. - -interpretation "Subset" 'subset A B = - (cic:/matita/sets/subset.con _ A B). - -definition intersection: ∀X. set X → set X → set X ≝ - λX.λA,B:set X.λx. x ∈ A ∧ x ∈ B. - -notation "hvbox(A break ∩ B)" with precedence 70 -for @{ 'intersection $A $B }. - -interpretation "Intersection" 'intersection A B = - (cic:/matita/sets/intersection.con _ A B). - -definition union: ∀X. set X → set X → set X ≝ λX.λA,B:set X.λx. x ∈ A ∨ x ∈ B. - -notation "hvbox(A break ∪ B)" with precedence 65 -for @{ 'union $A $B }. - -interpretation "Union" 'union A B = - (cic:/matita/sets/union.con _ A B). - -definition seq ≝ λX:Type.nat → X. - -definition nth ≝ λX.λA:seq X.λi.A i. - -notation "hvbox(A \sub i)" with precedence 100 -for @{ 'nth $A $i }. - -interpretation "nth" 'nth A i = - (cic:/matita/sets/nth.con _ A i). - -definition countable_union: ∀X. seq (set X) → set X ≝ - λX.λA:seq (set X).λx.∃j.x ∈ A \sub j. - -notation "∪ \sub (ident i opt (: ty)) B" with precedence 65 -for @{ 'big_union ${default @{(λ${ident i}:$ty.$B)} @{(λ${ident i}.$B)}}}. - -interpretation "countable_union" 'big_union η.t = - (cic:/matita/sets/countable_union.con _ t). - -definition complement: ∀X. set X \to set X ≝ λX.λA:set X.λx. x ∉ A. - -notation "A \sup 'c'" with precedence 100 -for @{ 'complement $A }. - -interpretation "Complement" 'complement A = - (cic:/matita/sets/complement.con _ A). - -definition inverse_image: ∀X,Y.∀f: X → Y.set Y → set X ≝ - λX,Y,f,B,x. f x ∈ B. - -notation "hvbox(f \sup (-1))" with precedence 100 -for @{ 'finverse $f }. - -interpretation "Inverse image" 'finverse f = - (cic:/matita/sets/inverse_image.con _ _ f). \ No newline at end of file diff --git a/helm/software/matita/dama/sigma_algebra.ma b/helm/software/matita/dama/sigma_algebra.ma deleted file mode 100644 index 94ceb923d..000000000 --- a/helm/software/matita/dama/sigma_algebra.ma +++ /dev/null @@ -1,40 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -set "baseuri" "cic:/matita/sigma_algebra/". - -include "topology.ma". - -record is_sigma_algebra (X:Type) (A: set X) (M: set (set X)) : Prop ≝ - { siga_subset: ∀B.B ∈ M → B ⊆ A; - siga_full: A ∈ M; - siga_compl: ∀B.B ∈ M → B \sup c ∈ M; - siga_enumerable_union: - ∀B:seq (set X).(∀i.(B \sub i) ∈ M) → (∪ \sub i B \sub i) ∈ M - }. - -record sigma_algebra : Type ≝ - { siga_carrier:> Type; - siga_domain:> set siga_carrier; - M: set (set siga_carrier); - siga_is_sigma_algebra:> is_sigma_algebra ? siga_domain M - }. - -(*definition is_measurable_map ≝ - λX:sigma_algebra.λY:topological_space.λf:X → Y. - ∀V. V ∈ O Y → f \sup -1 V ∈ M X.*) -definition is_measurable_map ≝ - λX:sigma_algebra.λY:topological_space.λf:X → Y. - ∀V. V ∈ O Y → inverse_image ? ? f V ∈ M X. - diff --git a/helm/software/matita/dama/topology.ma b/helm/software/matita/dama/topology.ma deleted file mode 100644 index f068fcbd5..000000000 --- a/helm/software/matita/dama/topology.ma +++ /dev/null @@ -1,45 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -set "baseuri" "cic:/matita/topology/". - -include "sets.ma". - -record is_topology (X) (A: set X) (O: set (set X)) : Prop ≝ - { top_subset: ∀B. B ∈ O → B ⊆ A; - top_empty: ∅︀ ∈ O; - top_full: A ∈ O; - top_intersection: ∀B,C. B ∈ O → C ∈ O → B ∩ C ∈ O; - top_countable_union: - ∀B.(∀i.(B \sub i) ∈ O) → (∪ \sub i (B \sub i)) ∈ O - }. - -record topological_space : Type ≝ - { top_carrier:> Type; - top_domain:> set top_carrier; - O: set (set top_carrier); - top_is_topological_space:> is_topology ? top_domain O - }. - -(*definition is_continuous_map ≝ - λX,Y: topological_space.λf: X → Y. - ∀V. V ∈ O Y → (f \sup -1) V ∈ O X.*) -definition is_continuous_map ≝ - λX,Y: topological_space.λf: X → Y. - ∀V. V ∈ O Y → inverse_image ? ? f V ∈ O X. - -record continuous_map (X,Y: topological_space) : Type ≝ - { cm_f:> X → Y; - cm_is_continuous_map: is_continuous_map ? ? cm_f - }. \ No newline at end of file