With df-rgr and df-rusgr, k-regularity of a (simple) graph is defined as
predicate resp. .
Instead of defining a predicate, an alternative could have been to define a
function that maps an extended nonnegative integer to the class of "graphs"
in which every vertex has the extended nonnegative integer as degree:
. This function, however, would not be
defined at least for (see rgrx0nd), because
is not a set
(see rgrprcx). It is expected that this function is not defined for every
(how could this be proven?).