**Description: **Define the *Hartogs
function* , which maps all sets to the smallest
ordinal that cannot be injected into the given set. In the important
special case where is an ordinal, this is the *cardinal successor*
operation.
Traditionally, the Hartogs number of a set is written
and the cardinal successor ; we
use functional notation for
this, and cannot use the aleph symbol because it is taken for the
enumerating function of the infinite initial ordinals df-aleph 7573.
Some authors define the Hartogs number of a set to be the least
*infinite* ordinal which does not inject into it, thus causing the range
to consist only of alephs. We use the simpler definition where the
value can be any successor cardinal. (Contributed by Stefan O'Rear,
11-Feb-2015.) |