English
Bounded limit-recursive construction: recursion over ordinals below a fixed limit l with explicit bound on the domain.
Русский
Ограниченная по пределу конструкция рекурсии по ординалам ниже заданного предела l с явным ограничением области определения.
LaTeX
$${l : Ordinal} \to \mathrm{Limit} \text{(IsSuccLimit l)} \, \Rightarrow \, \text{boundedLimitRecOn}(l)(lLim)(motive)(o)\text{ ... }$$
Lean4
/-- Bounded recursion on ordinals. Similar to `limitRecOn`, with the assumption `o < l`
added to all cases. The final term's domain is the ordinals below `l`. -/
@[elab_as_elim]
def boundedLimitRecOn {l : Ordinal} (lLim : IsSuccLimit l) {motive : Iio l → Sort*} (o : Iio l)
(zero : motive ⟨0, lLim.bot_lt⟩) (succ : (o : Iio l) → motive o → motive ⟨succ o, lLim.succ_lt o.2⟩)
(limit : (o : Iio l) → IsSuccLimit o.1 → (Π o' < o, motive o') → motive o) : motive o :=
limitRecOn (motive := fun p ↦ (h : p < l) → motive ⟨p, h⟩) o.1 (fun _ ↦ zero)
(fun o ih h ↦ succ ⟨o, _⟩ <| ih <| (lt_succ o).trans h) (fun _o ho ih _ ↦ limit _ ho fun _o' h ↦ ih _ h _) o.2
