There are other definitions of infinity on the complex plane: Benoît has for example defined the circle at infinity, with an infinite number of points at infinity (see ~ bj-inftyexpidisj <http://us2.metamath.org:88/mpeuni/bj-inftyexpidisj.html>), and the (single) point at infinity of the complex projective line (~ df-bj-infty <http://us2.metamath.org:88/mpeuni/df-bj-infty.html>). These might be used as more general versions of infinity, and we could then identify the current `+oo` and `-oo` with the corresponding points at infinity in direction 0 and π.
Glauco, can you give the actual counter example you tried to prove in the first place? Isn't it possible to prove it within RR, using `abs`, without any need to consider `CC`? -- 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/8b0fda14-cd38-1f3b-72d8-febc998885db%40gmx.net.
