On 1/5/22 11:54 AM, Glauco wrote:
1. the "standard" theory works perfectly fine without assuming plus
infinity not being a complex number. Thus, |- -. +oo e. CC should NOT
be a theorem in set.m
As far as I could tell from a quick glance, everything would work if +oo
is defined to be _i and -oo is defined to be -u _i .
At least that seems like it from the "requiring only that +∞ be a set
not in ℝ" language in http://us.metamath.org/mpeuni/df-pnf.html and,
backing it up, that df-pnf is only used in
http://us.metamath.org/mpeuni/pnfnre.html and
http://us.metamath.org/mpeuni/mnfnre.html (and a third one trivially
satisfied by anything used to define RR* the way we do) and that other
usages go via pnfnre .
--
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/8d853c6e-e4ae-0568-f01c-8eceddbcf31a%40panix.com.
