English
Let f be a family of ordinal-valued functions indexed by ι. Then the derivative at the successor of o is the least fixed point, taken pointwise after advancing the argument by one: derivFamily f (succ o) = nfpFamily f (succ (derivFamily f o)).
Русский
Пусть f будет семейством функций ι → Ordinal → Ordinal. Тогда производная семейства на succ(o) равна наименьшей фиксированной точке семейства после приращения аргумента на единицу: derivFamily f (succ o) = nfpFamily f (succ (derivFamily f o)).
LaTeX
$$$$ \forall o, \ derivFamily f(\operatorname{succ} o) = \operatorname{nfpFamily} f(\operatorname{succ}(\derivFamily f o)). $$$$
Lean4
@[simp]
theorem derivFamily_succ (f : ι → Ordinal → Ordinal) (o) :
derivFamily f (succ o) = nfpFamily f (succ (derivFamily f o)) :=
limitRecOn_succ ..
