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
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/6b0c63be-7042-48d5-a981-3fbc30675261n%40googlegroups.com.
