From: Enrico Tassi <enrico.tassi@inria.fr>
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: 0.4.95@7852~43
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=72a05c70f5ab9dabb704f1dc334920b10a8f4bb9

reorganization of the whole story, the root dir contains the algebraic structure
---

diff --git a/matita/dama/classical_pointfree/ordered_sets.ma b/matita/dama/classical_pointfree/ordered_sets.ma
new file mode 100644
index 000000000..18658cf7a
--- /dev/null
+++ b/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/matita/dama/classical_pointfree/ordered_sets2.ma b/matita/dama/classical_pointfree/ordered_sets2.ma
new file mode 100644
index 000000000..dafa0df4f
--- /dev/null
+++ b/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/matita/dama/classical_pointwise/sets.ma b/matita/dama/classical_pointwise/sets.ma
new file mode 100644
index 000000000..ec6a1c774
--- /dev/null
+++ b/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/matita/dama/classical_pointwise/sigma_algebra.ma b/matita/dama/classical_pointwise/sigma_algebra.ma
new file mode 100644
index 000000000..21db34e38
--- /dev/null
+++ b/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/matita/dama/classical_pointwise/topology.ma b/matita/dama/classical_pointwise/topology.ma
new file mode 100644
index 000000000..c5ba9bbd6
--- /dev/null
+++ b/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/matita/dama/ordered_groups.ma b/matita/dama/ordered_groups.ma
index a9912d43f..10e8f189a 100644
--- a/matita/dama/ordered_groups.ma
+++ b/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/matita/dama/ordered_sets.ma b/matita/dama/ordered_sets.ma
index 62b934865..dcae29e18 100644
--- a/matita/dama/ordered_sets.ma
+++ b/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/matita/dama/ordered_sets2.ma b/matita/dama/ordered_sets2.ma
deleted file mode 100644
index a8050ec21..000000000
--- a/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/matita/dama/sets.ma b/matita/dama/sets.ma
deleted file mode 100644
index ec6a1c774..000000000
--- a/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/matita/dama/sigma_algebra.ma b/matita/dama/sigma_algebra.ma
deleted file mode 100644
index 94ceb923d..000000000
--- a/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/matita/dama/topology.ma b/matita/dama/topology.ma
deleted file mode 100644
index f068fcbd5..000000000
--- a/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