English
For lLim a succ-limit, the value at a limit index o is given by H3 o oLim applied to the function x ↦ boundedLimitRecOn at x.
Русский
Пусть lLim — succ-предел; тогда на предельном индексе o значение равно H3 o oLim от функции x ↦ boundedLimitRecOn(l, lLim, motive, x, H1, H2, H3).
LaTeX
$$$$ \forall l\ (lLim : IsSuccLimit l) \ {motive} (o\ H_1 H_2 H_3 oLim):\; \mathrm{boundedLimitRecOn}(l, lLim, motive)\; o\ H_1 H_2 H_3 = H_3\ o\ oLim\ (\lambda x\ _ \mapsto \mathrm{boundedLimitRecOn}(l, lLim, motive, x, H_1, H_2, H_3)) $$$$
Lean4
theorem boundedLimitRec_limit {l} (lLim : IsSuccLimit l) {motive} (o H₁ H₂ H₃ oLim) :
@boundedLimitRecOn l lLim motive o H₁ H₂ H₃ = H₃ o oLim (fun x _ ↦ @boundedLimitRecOn l lLim motive x H₁ H₂ H₃) :=
by
rw [boundedLimitRecOn, limitRecOn_limit]
rfl
