English
If b carries the IsPredPrelimit property, then the recursively defined prelimitRecOn at b coincides with the given isPredPrelimit data applied to b and hb, with the recursive clause carried by prelimitRecOn on smaller arguments.
Русский
Если b удовлетворяет свойству IsPredPrelimit, то рассчитанный по рекурсии prelimitRecOn на b совпадает с данным isPredPrelimit, применённым к b и hb, причём рекурсивное звено задаётся через предшественник.
LaTeX
$$$\\text{hb} : \\mathrm{IsPredPrelimit}(b) \\;\\Rightarrow\\; \\mathrm{prelimitRecOn}(b) = \\mathrm{isPredPrelimit}(b, \\mathrm{hb}) \\big( \\lambda x, - \\mapsto \\mathrm{prelimitRecOn}(x) \\big)$$$
Lean4
@[simp]
theorem prelimitRecOn_of_isPredPrelimit (hb : IsPredPrelimit b) :
prelimitRecOn b pred isPredPrelimit = isPredPrelimit b hb fun x _ ↦ prelimitRecOn x pred isPredPrelimit :=
SuccOrder.prelimitRecOn_of_isSuccPrelimit _ _ hb.dual
