English
Limit recursion at a successor step: limitRecOn (succ o) H1 H2 H3 = H2 o (limitRecOn o H1 H2 H3).
Русский
Рекурсия по пределу на шаге-суктора: limitRecOn (succ o) H1 H2 H3 = H2 o (limitRecOn o H1 H2 H3).
LaTeX
$$$\forall o,\ limitRecOn(\mathrm{succ}\, o)\ H_1\ H_2\ H_3 = H_2\ o\ (\mathrm{limitRecOn}\ o\ H_1\ H_2\ H_3)$$$
Lean4
/-- Main induction principle of ordinals: if one can prove a property by
induction at successor ordinals and at limit ordinals, then it holds for all ordinals. -/
@[elab_as_elim]
def limitRecOn {motive : Ordinal → Sort*} (o : Ordinal) (zero : motive 0) (succ : ∀ o, motive o → motive (succ o))
(limit : ∀ o, IsSuccLimit o → (∀ o' < o, motive o') → motive o) : motive o :=
SuccOrder.limitRecOn o (fun _a ha ↦ ha.eq_bot ▸ zero) (fun a _ ↦ succ a) limit
