It's better to have $\pm\infty \notin \CC$ ("plus/minus infinity not in
CC"), even though \pm\infty are used in a real context, so generally not
together with complex numbers, so $\pm\infty \notin \RR$ would probably
suffice. This avoids more potential clashes. We can "detach" from the
proof of $+\infty \notin \RR$ the intermediate step $+\infty \notin \CC$
although it would probably not be used much, for the above reason.
Note that \pm\infinity on the one hand, and \infinity on the other hand,
are the points added in the two standard compactifications of \RR, where
\lim_{x \to a} can be interpreted as a limit in a topological space in the
same way regardless of a being finite or infinite. Note that in set.mm,
where we like genuine inclusions, \infty should be "the same" point in the
one-point (or "Alexandroff") compactification of \C, yielding the real and
complex projective lines (complex projective line = Riemann sphere). I
developped in my mathbox a proposal where all these spaces fit well
together, with genuine inclusions: see the section in my mathbox titled
"Extended real and complex numbers, real and complex projectives lines".
(I just noticed the typo "projectives", which I'll fix soon.)
Benoît
On Wednesday, January 5, 2022 at 10:49:03 PM UTC+1 Alexander van der Vekens
wrote:
> Maybe the current definition might leave open the possibility to use it
> for the complex case as mentioned in the Wikipedia article in the future...
>
> On Wednesday, January 5, 2022 at 10:43:16 PM UTC+1 Alexander van der
> Vekens wrote:
>
>> Maybe Wikipedia (https://en.wikipedia.org/wiki/Infinity#Calculus) gives
>> some hints:
>> * In real analysis <https://en.wikipedia.org/wiki/Real_analysis>, the
>> symbol , called "infinity", is used to denote an unbounded limit
>> <https://en.wikipedia.org/wiki/Limit_of_a_function>. The notation x -->
>> +oo means that x increases without bound, and x --> -oo means that x
>> decreases
>> without bound.
>> * In complex analysis <https://en.wikipedia.org/wiki/Complex_analysis>
>> the symbol oo, called "infinity", denotes an unsigned infinite limit
>> <https://en.wikipedia.org/wiki/Limit_(mathematics)>. x --> oo means that
>> the magnitude |x| of x grows beyond any assigned value.
>>
>> Especially in the real case, we have the definition of superior limit
>> limsup which can take the values -oo and +oo, see ~ limsupcl . As far as I
>> know, there is nothing in set.mm corresponding to the complex case.
>>
>>
>>
--
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/9abd69c6-91ed-49a2-8f12-d84a38d053cfn%40googlegroups.com.
