limitRecOn — Mathlib

English

If b is minimal, the Succ limit recursion equals isMin at b.

Русский

Если b минимален, предел-рекурсия Succ равна isMin(b).

LaTeX

$$$\\mathrm{isSuccLimitRecOn}(b, isMin, succ, isSuccLimit) = \\mathrm{isMin}(b,hb)$ for hb: IsMin(b).$$$

Lean4

/-- Recursion principle on a well-founded partial `SuccOrder`, separating out the case of a
minimal element. -/
@[elab_as_elim]
noncomputable def limitRecOn : motive b :=
  prelimitRecOn b succ fun a ha IH ↦ if h : IsMin a then isMin a h else isSuccLimit a (ha.isSuccLimit_of_not_isMin h) IH

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