From: Claudio Sacerdoti Coen Date: Wed, 31 May 2006 15:54:25 +0000 (+0000) Subject: Committed a first experiment in the formalization of Lebesgue dominated X-Git-Tag: 0.4.95@7852~1374 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b1ee9ef71c8badde1b783e0e0296a4e7d87a8aa4;p=helm.git Committed a first experiment in the formalization of Lebesgue dominated convergence theorem: basic set theory and classical topology definitions. --- diff --git a/matita/dama/makefile b/matita/dama/makefile new file mode 100644 index 000000000..39d64a952 --- /dev/null +++ b/matita/dama/makefile @@ -0,0 +1,33 @@ +H=@ + +RT_BASEDIR=../ +OPTIONS=-bench +MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS) +CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) +MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS) +CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) + +devel:=$(shell basename `pwd`) + +all: preall + $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel) +clean: preall + $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel) +cleanall: preall + $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all + +all.opt opt: preall + $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel) +clean.opt: preall + $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel) +cleanall.opt: preall + $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all + +%.mo: preall + $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@ +%.mo.opt: preall + $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@ + +preall: + $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel) + diff --git a/matita/dama/sets.ma b/matita/dama/sets.ma new file mode 100644 index 000000000..ec6a1c774 --- /dev/null +++ b/matita/dama/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/matita/dama/topology.ma b/matita/dama/topology.ma new file mode 100644 index 000000000..3a7ec0da7 --- /dev/null +++ b/matita/dama/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 "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; + top_O: set (set top_carrier); + top_is_topological_space:> is_topology ? top_domain top_O + }. + +(*definition is_continuous_map ≝ + λX,Y: topological_space.λf: X → Y. + ∀V. V ∈ top_O Y → (f \sup -1) V ∈ top_O X.*) +definition is_continuous_map ≝ + λX,Y: topological_space.λf: X → Y. + ∀V. V ∈ top_O Y → inverse_image ? ? f V ∈ top_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