Description: Define plus infinity.
Note that the definition is arbitrary, requiring
only that +∞ be a set not in ℝ and different from -∞
(df-mnf 9956). 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 9960,
mnfnre 9961, and pnfnemnf 9973.
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.) |