Thanks Glauco, Ok, I see that your new formulation would be provable, since you have already proven ` ( limsup ` (/) ) = -oo ` in ~ limsup0.
I suppose you're just being curious about out-of-domain behavior here, and whether or not you are able to prove this counter example shall not have any impact on the broader picture, like measure theory or integration. Did you see ~ lmdvglim <http://us2.metamath.org:88/mpeuni/lmdvglim.html> ? It states that if a monotonic sequence does not converge in the real numbers in the sense of ~~> , then it converges to +oo in the topology of the extended numbers. Maybe it could be related with what you're interested in. Also, in his Mathbox, and commented out, Mario has a sketch of definition of an Alexandroff extension, using `~P U. X` (~ alextop; see also ~ dfac14lem <http://us2.metamath.org:88/mpeuni/dfac14lem.html> and ~ kelac2lem <http://us2.metamath.org:88/mpeuni/kelac2lem.html>). I think those would be interesting starting points to define one-point compactifications, and apply them to the complex plane. BR, _ Thierry -- 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/45dfa7ac-aa2e-40f3-f1c9-942c9a1d8ce2%40gmx.net.
