Committed a first experiment in the formalization of Lebesgue dominated

convergence theorem: basic set theory and classical topology definitions.

diff --git a/helm/software/matita/dama/makefile b/helm/software/matita/dama/makefile
new file mode 100644 (file)
index 0000000..39d64a9
--- /dev/null
+++ b/helm/software/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/helm/software/matita/dama/sets.ma b/helm/software/matita/dama/sets.ma
new file mode 100644 (file)
index 0000000..ec6a1c7
--- /dev/null
+++ b/helm/software/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/helm/software/matita/dama/topology.ma b/helm/software/matita/dama/topology.ma
new file mode 100644 (file)
index 0000000..3a7ec0d
--- /dev/null
+++ b/helm/software/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