On Thursday, January 6, 2022 at 4:54:19 AM UTC+1 Thierry Arnoux wrote: > 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 π. > Thanks for mentioning it. It is already in set.mm as: df-bj-pinfty $a |- pinfty = ( inftyexpi ` 0 ) $. df-bj-minfty $a |- minfty = ( inftyexpi ` _pi ) $.
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/ffdd7b67-0954-4b46-b0b8-480cf74904a6n%40googlegroups.com.
