| Description: Define plus infinity.
Note that the definition is arbitrary, requiring
only that +∞ be a set not in ℝ and different from -∞
(df-mnf 7957). We use 𝒫 ∪ ℂ to make it independent of the
construction of ℂ, and Cantor's Theorem will
show that it is
different from any member of ℂ and therefore
ℝ. See pnfnre 7961
and mnfnre 7962, and we'll also be able to prove +∞ ≠ -∞.
A simpler possibility is to define +∞ as
ℂ and -∞ as
{ℂ}, but that approach requires the Axiom of
Regularity to show
that +∞ and -∞
are different from each other and from all
members of ℝ. (Contributed by NM,
13-Oct-2005.)
(New usage is discouraged.) |
