English
There is a recursion principle on a well-founded PredOrder that separates out maximal elements. The motive at b is determined by the maximal-case function isMax and the remaining pred-case data isPredLimit.
Русский
Существует принцип рекурсии по хорошо основанному порядку предшественников, выделяющий максимальные элементы. Мотив на b задаётся через максимальный случай isMax и регрессии предшественников isPredLimit.
LaTeX
$$$\\text{limitRecOn}(b) : MOTIVE(b) \\,=\, \\text{SuccOrder.limitRecOn} (α := α^{op})\n b \n isMax \n pred \n (\\lambda a ha. \\text{isPredLimit}(a, ha.dual))$$$
Lean4
/-- Recursion principle on a well-founded partial `PredOrder`, separating out the case of a
maximal element. -/
@[elab_as_elim]
noncomputable def limitRecOn : motive b :=
SuccOrder.limitRecOn (α := αᵒᵈ) b isMax pred (fun a ha => isPredLimit a ha.dual)
