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 (nnsscn10273), in contrast to the more elementary
ordinal natural numbers , df-om6447). See nnind10286 for the
principle of mathematical induction. See dfnn210281 for a slight variant.
See df-n010526 for the set of nonnegative integers . See dfn210538
defined in terms of .
This is a technical definition that helps us avoid the Axiom of Infinity
ax-inf27794 in certain proofs. For a more conventional
definition ("the smallest set of reals containing as well as the
successor of every member") see dfnn310282. (Contributed by NM,
10-Jan-1997.) (Revised by Mario Carneiro,