X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fclassical_pointfree%2Fordered_sets.ma;h=2630da77c6474b93a99281982f1edc229ff27ae8;hb=10f29fdd78ee089a9a94446207b543d33d6c851c;hp=18658cf7a9d8c964aa588c2692dde6369e488cc0;hpb=fdcfbe23f5e11b1856ca6adbc78e5374b493d199;p=helm.git

diff --git a/helm/software/matita/dama/classical_pointfree/ordered_sets.ma b/helm/software/matita/dama/classical_pointfree/ordered_sets.ma
index 18658cf7a..2630da77c 100644
--- a/helm/software/matita/dama/classical_pointfree/ordered_sets.ma
+++ b/helm/software/matita/dama/classical_pointfree/ordered_sets.ma
@@ -12,11 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/classical_pointwise/ordered_sets/".
 
-include "ordered_sets.ma".
 
-record is_dedekind_sigma_complete (O:ordered_set) : Type ≝
+include "excess.ma".
+
+record is_dedekind_sigma_complete (O:excess) : 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'.
@@ -30,7 +30,7 @@ record is_dedekind_sigma_complete (O:ordered_set) : Type ≝
  }.
 
 record dedekind_sigma_complete_ordered_set : Type ≝
- { dscos_ordered_set:> ordered_set;
+ { dscos_ordered_set:> excess;
    dscos_dedekind_sigma_complete_properties:>
     is_dedekind_sigma_complete dscos_ordered_set
  }.
@@ -155,7 +155,7 @@ lemma inf_respects_le:
 qed. 
 
 definition is_sequentially_monotone ≝
- λO:ordered_set.λf:O→O.
+ λO:excess.λf:O→O.
   ∀a:nat→O.∀p:is_increasing ? a.
    is_increasing ? (λi.f (a i)).
 
@@ -320,10 +320,10 @@ notation "hvbox(〈a〉)"
 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 _).
+= (cic:/matita/classical_pointfree/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 _).
+= (cic:/matita/classical_pointfree/ordered_sets/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _).
 
 theorem eq_f_sup_sup_f:
  ∀O':dedekind_sigma_complete_ordered_set.