English
Let α be a partially ordered set with a predecessor operation and a well-founded predecessor order. Suppose pred assigns to any a with a not minimal element a motive for Order.pred a, and isPredPrelimit provides a way to compute motive at a from all larger elements. Then there exists a recursion principle prelimitRecOn that computes the motive at any b by stepping through predecessors according to pred, i.e., motive at b is determined by the motive at Order.pred b via the provided pred/IsPredPrelimit data.
Русский
Пусть α – частично упорядоченное множество с операцией предшественника и хорошо упорядоченным порядком предшественников. Пусть pred задаёт для каждого a с неминимальным элементом мотив для Order.pred a, а isPredPrelimit задаёт способ вычисления мотива для a через мотивацию большего элемента. Тогда существует принцип рекурсии prelimitRecOn, который вычисляет мотив на b, переходя по предшественникам через pred, т.е. мотив в b определяется мотивом в Order.pred b через заданные pred/isPredPrelimit.
LaTeX
$$$\\exists \\text{motive}: α \\to \\mathsf{Sort}^* , \\text{pred} : \\forall a, \\neg \\mathrm{IsMin}(a) \\to \\text{motive}(a) \\to \\text{motive}(\\mathrm{Order.pred}\,a) \\, \\land \\, \\text{isPredPrelimit} : \\forall a, \\mathrm{IsPredPrelimit}(a) \\to (\\forall b > a, \\text{motive}(b) ) \\to \\text{motive}(a) \\, \\Rightarrow \\, \\text{prelimitRecOn}(b) \\text{ exists and satisfies the recursion } \mathrm{prelimitRecOn}(b) = \\text{SuccOrder.prelimitRecOn} (\\alpha := α^{{op}}) (b) \\; pred \\; (\\lambda a. \\lambda ha. \\text{isPredPrelimit}(a) \\, (ha.dual))$$$
Lean4
/-- Recursion principle on a well-founded partial `PredOrder`. -/
@[elab_as_elim]
noncomputable def prelimitRecOn : motive b :=
SuccOrder.prelimitRecOn (α := αᵒᵈ) b pred (fun a ha => isPredPrelimit a ha.dual)
