Finite ordinal (source code)

= Finite ordinal
{title2=$n<\omega$}

A finite <ordinal> is the order type of a finite <well-order>; in the von Neumann representation it is one of $0,1,2,\ldots$. They are exactly the <ordinals> $x$ such that $x$ and each member of $x$ are either zero or <successor ordinals>. If an <ordinal> is infinite, it either is the nonzero limit $\omega$ or contains $\omega$ as a member, so it fails this test. Thus the <finite ordinals> give the usual representation of the <natural numbers>.