X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fclassical_pointfree%2Fordered_sets.ma;h=b42a8c44b4d99d65b0e4a3cda37e531a24c0d681;hb=feaabb3c45906fafb4b6eb3fb10add6e6da6069b;hp=127bbf69623e8830c0f380983c2f375989491b0c;hpb=39c55604f8114e2e8f9f9769acd328de8f19c7e4;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 127bbf696..b42a8c44b 100644
--- a/helm/software/matita/dama/classical_pointfree/ordered_sets.ma
+++ b/helm/software/matita/dama/classical_pointfree/ordered_sets.ma
@@ -14,9 +14,9 @@
 
 set "baseuri" "cic:/matita/classical_pointwise/ordered_sets/".
 
-include "ordered_set.ma".
+include "excedence.ma".
 
-record is_dedekind_sigma_complete (O:ordered_set) : Type ≝
+record is_dedekind_sigma_complete (O:excedence) : 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:> excedence;
    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:excedence.λf:O→O.
   ∀a:nat→O.∀p:is_increasing ? a.
    is_increasing ? (λi.f (a i)).