Description: Define a function
recs  on ,
the class of ordinal
numbers, by transfinite recursion given a rule which sets the next
value given all values so far. See df-rdg 6631 for more details on why
this definition is desirable. Unlike df-rdg 6631 which restricts the
update rule to use only the previous value, this version allows the
update rule to use all previous values, which is why it is
described
as "strong", although it is actually more primitive. See recsfnon 6624 and
recsval 6625 for the primary contract of this definition.
EDITORIAL: there are several existing versions of this
construction
without the definition, notably in ordtype 7461, zorn2 8346, and
dfac8alem 7870. (Contributed by Stefan O'Rear,
18-Jan-2015.)
(New usage is discouraged.) |