English
There is a predecessor-based recursion construction isPredPrelimitRecOn on α, defined by applying the successor-based recursion on the dual order with the predicate pred for predecessors.
Русский
Существует построение исчисления предшественников через рекурсию на двойственном порядке с pred.
LaTeX
$$$\\mathrm{isPredPrelimitRecOn}(b) = \\mathrm{isSuccPrelimitRecOn}_{\\alpha^{op}}(b, \\mathrm{pred}, \\lambda a,h a. \\mathrm{isPredPrelimit}(a,h.dual)).$$$
Lean4
/-- A value can be built by building it on predecessors and predecessor pre-limits. -/
@[elab_as_elim]
noncomputable def isPredPrelimitRecOn : motive b :=
isSuccPrelimitRecOn (α := αᵒᵈ) b pred (fun a ha ↦ isPredPrelimit a ha.dual)
