Superior limit

[Benoit]

After a recent discussion on github about Dedekind and Cauchy completeness in intuitionistic logic, I thought a bit about how to prove the second from the first, that is, existence of certain limits from existence of certain supremums (suprema).  It seems best to use the intermediate step of superior limit.  In set.mm, it is defined as df-limsup, but this is for the superior limit of a real sequence.  Wouldn't it be more in set.mm's spirit to define it more generally ?  For instance, the superior limit of a subset in a totally ordered set ?

Has someone thought of it or done it in his mathbox or without uploading it ?  One should define the order topology, probably using set.mm's structures with which I'm not familiar, and also the derived set of a subset of a topological space (maybe already done somewhere?).

Just for the record:

* if (R, >) is a totally ordered set, then the order topology has basis the set of ]a, b[ with a, b \in R;

* if X is a topological space and A \subseteq X, then A' := { x \in X \mid x \in \closure{A \setminus {x} }

* if (R, <) is a totally ordered set, then limsup A := sup A' (I don't know if there is a +\infty(R) and a -\infty(R) defined for all totally ordered sets like for the reals).

Thanks,

Benoît