isSuccLimitRecOn — Mathlib

English

If b is a successor-limit, then the limit recursion on b reduces to the isSuccLimit data at b.

Русский

Если b является пределом перехода к следующему элементу, предел продолжения сводится к данным IsSuccLimit на b.

LaTeX

$$$\\mathrm{isSuccLimitRecOn}(b,\; isMin,\; succ,\; isSuccLimit) = \\mathrm{isSuccLimit}(b,hb)$ where $hb$ is IsSuccLimit(b).$$

Lean4

/-- A value can be built by building it on minimal elements, successors, and successor limits. -/
@[elab_as_elim]
noncomputable def isSuccLimitRecOn : motive b :=
  isSuccPrelimitRecOn b succ fun a ha ↦ if h : IsMin a then isMin a h else isSuccLimit a (ha.isSuccLimit_of_not_isMin h)

Похожие утверждения