Description: Define the set of
positive integers. Some authors, especially in analysis
books, call these the natural numbers, whereas other authors choose to
include 0 in their definition of natural numbers. Note that  is a
subset of complex numbers (nnsscn 11025), in contrast to the more elementary
ordinal natural numbers  , df-om 7066). See nnind 11038 for the
principle of mathematical induction. See df-n0 11293 for the set of
nonnegative integers  . See dfn2 11305 for defined in terms of
.
This is a technical definition that helps us avoid the Axiom of Infinity
ax-inf2 8538 in certain proofs. For a more conventional
and intuitive
definition ("the smallest set of reals containing  as well as the
successor of every member") see dfnn3 11034 (or its slight variant dfnn2 11033).
(Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro,
3-May-2014.) |
