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'.
}.
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
}.
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)).