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